lplfitch (30jun13)

git-svn-id: svn://tug.org/texlive/trunk@31077 c570f23f-e606-0410-a88d-b1316a301751

1 files changed, 131 insertions, 0 deletions

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'.