From b7e38f0686232dbecee5d93bdabbdfcbee625610 Mon Sep 17 00:00:00 2001 From: Karl Berry Date: Tue, 2 Jul 2013 23:21:33 +0000 Subject: lplfitch (30jun13) git-svn-id: svn://tug.org/texlive/trunk@31077 c570f23f-e606-0410-a88d-b1316a301751 --- Master/texmf-dist/tex/latex/lplfitch/lplfitch.sty | 131 ++++++++++++++++++++++ 1 file changed, 131 insertions(+) create mode 100644 Master/texmf-dist/tex/latex/lplfitch/lplfitch.sty (limited to 'Master/texmf-dist/tex/latex/lplfitch') diff --git a/Master/texmf-dist/tex/latex/lplfitch/lplfitch.sty b/Master/texmf-dist/tex/latex/lplfitch/lplfitch.sty new file mode 100644 index 00000000000..1ca3f348de3 --- /dev/null +++ b/Master/texmf-dist/tex/latex/lplfitch/lplfitch.sty @@ -0,0 +1,131 @@ +%% +%% This is file `lplfitch.sty', +%% generated with the docstrip utility. +%% +%% The original source files were: +%% +%% lplfitch.dtx (with options: `package') +%% +%% This is a generated file. +%% +%% Copyright (C) 2013 by John Etchemendy, Dave Barker-Plummer and Richard Zach +%% +%% This file may be distributed and/or modified under the conditions of +%% the LaTeX Project Public License, either version 1.2 of this license +%% or (at your option) any later version. The latest version of this +%% license is in: +%% +%% http://www.latex-project.org/lppl.txt +%% +%% and version 1.2 or later is part of all distributions of LaTeX version +%% 1999/12/01 or later. +%% +\NeedsTeXFormat{LaTeX2e}[1999/12/01] +\ProvidesPackage{lplfitch} + [2013/05/16 v0.9 LPL Fitch style] +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{lplfitch}[2013/05/07 -- Fitch Proofs a la LPL] +\newcommand*{\formula}[1]{\ensuremath{\sf{#1}}} +\newcommand*\lif{\rightarrow} +\newcommand*\liff{\leftrightarrow} +\newcommand*\lfalse{\bot} +\newcommand*\lall{\forall} +\newcommand*\lis{\exists} +\newcommand*{\quant}[3]{#1 #2\;#3} +\newcommand*{\exi}[2]{\quant{\lis}{#1}{#2}} +\newcommand*{\uni}[2]{\quant{\lall}{#1}{#2}} +\newcommand*\intro[1]{\formula{#1\,}{\bf Intro:}} +\newcommand*\elim[1]{\formula{#1\,}{\bf Elim:}} + +\newcommand*\landi[1]{\intro{\land} #1} +\newcommand*\lande[1]{\elim{\land} #1} +\newcommand*\lori[1]{\intro{\lor} #1} +\newcommand*\lore[3]{\elim{\lor} #1, #2, #3} +\newcommand*\lnoti[1]{\intro{\lnot} #1} +\newcommand*\lnote[1]{\elim{\lnot} #1} + +\newcommand*\lfalsei[2]{\intro{\lfalse} #1, #2} +\newcommand*\lfalsee[1]{\elim{\lfalse} #1} + +\newcommand*\lifi[1]{\intro{\lif} #1} +\newcommand*\life[2]{\elim{\lif} #1, #2} + +\newcommand*\liffi[2]{\intro{\liff} #1, #2} +\newcommand*\liffe[2]{\elim{\liff} #1, #2} + +\newcommand*\reit[1]{{\bf Reit:} #1} + +\newcommand*\eqi[0]{$=\,${\bf Intro}} +\newcommand*\eqe[2]{\elim{=} #1, #2} + +\newcommand*\lalli[1]{\intro{\lall} #1} +\newcommand*\lalle[1]{\elim{\lall} #1} + +\newcommand*\lexii[1]{\intro{\lis} #1} +\newcommand*\lexie[2]{\elim{\lis} #1, #2} +\newlength{\fitchargwidth} +\setlength{\fitchargwidth}{3.5in} +\newlength{\fitchprfwidth} +\setlength{\fitchprfwidth}{3.0in} +\newlength{\fitchctxwidth} +\setlength{\fitchctxwidth}{1in} +\newlength{\fitchsep} +\setlength{\fitchsep}{10pt} +\newcommand{\fitchctx}[1]{% +\advance \fitchctxwidth by -\fitchsep% +\advance \fitchctxwidth by .5pt% +\begin{tabular}[t]{r@{}|p{\fitchctxwidth}@{}l} + \phantom{\slider} \\[-1.75ex] + #1 \\[-1.75ex] & & + \end{tabular} +\advance \fitchctxwidth by \fitchsep% +\advance \fitchctxwidth by -.5pt% +} +\newcommand{\fitchprf}[2]{% +\advance \fitchprfwidth by -\fitchsep% +\advance \fitchprfwidth by .5pt% +\hspace*{.35em}% +\begin{tabular}[t]{|p{0pt}@{}p{\fitchprfwidth}@{\hspace*{\fitchsep}}l} + \multicolumn{3}{@{}l@{}}{\ }\\[-2.35ex] + #1 \\ + \ \\[-2.5ex] \cline{1-1}\\[-2ex] + #2 \\ \multicolumn{3}{@{}l@{}} \ \\[-2.35ex] + \end{tabular} +\advance \fitchprfwidth by \fitchsep% +} +\newcommand{\fitcharg}[2]{ +\advance \fitchargwidth by -\fitchsep% +\hspace*{.35em} +\begin{tabular}[t]{|p{\fitchsep}@{}p{\fitchargwidth}@{}} +\multicolumn{2}{@{}l@{}}{\ }\\[-2.35ex] +#1 \\ +\ \\[-2.5ex] \cline{1-1}\\[-2ex] + #2 \\ \multicolumn{2}{@{}l@{}} \ \\[-2.35ex] +\end{tabular} +} +\newcommand*{\slider}{\mbox{$\triangleright \;$}} +\def\pline{\@ifnextchar[\@plinenum{\@plinenum[\@empty]}} +\def\@plinenum[#1]#2{\@ifnextchar[{\@plinex{#1}{#2}}{% + \@plinex{#1}{#2}[\@empty]}} +\def\@plinex#1#2[#3]{ & #1\formula{\; #2} & #3} +\newcommand*\fpline{\slider\pline} +\newcommand*{\tline}[2][{}]{ & #1\hspace{.6em}{#2}} +\newcommand*{\nline}[2][{}]{ & #1\formula{\;#2}} +\newcommand*{\jline}[2][{}]{\nline#2 & #1} +\newcommand*{\fline}[1]{\slider \jline#1} +\newcommand*{\ellipsesline}[0]{\nline{\;\raise.65ex\hbox{\vdots}}} +\newcommand{\subproof}[2]{&\fitchprf{#1}{#2}\\} +\newcommand{\boxedsubproof}[4][{}]{ + \subproof{\nline[#1]{\fbox{\formula{#2}}\;#3}}{#4} +} +\newcommand{\brokenform}[2]{ + \advance\fitchprfwidth by-\fitchsep + \begin{tabular}[c]{rp{\fitchprfwidth}} + \multicolumn{1}{p{\fitchprfwidth}@{}}{\formula{#1}}\\ + \formula{#2} + \end{tabular} + \advance\fitchprfwidth by\fitchsep +} +\endinput +%% +%% End of file `lplfitch.sty'. -- cgit v1.2.3