lplfitch (30jun13)

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

8 files changed, 1030 insertions, 1 deletions

diff --git a/Master/texmf-dist/doc/latex/lplfitch/README b/Master/texmf-dist/doc/latex/lplfitch/README
new file mode 100644
index 00000000000..c89659a03b8
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/lplfitch/README
@@ -0,0 +1,42 @@
+lplfitch
+========
+
+LaTeX package for typesetting Fitch-style proofs a la Language, Proof, 
+and Logic, a logic textbook by Jon Barwise and John Etchemendy. It was 
+originally written by John Etchemendy, with modifications by 
+Dave Barker-Plummer and Richard Zach.
+
+https://github.com/rzach/lplfitch
+
+Installation
+------------
+
+Run latex on lplfitch.ins to produce lplfitch.sty
+
+Run latex on lplfitch.dxt to produce the documentation.
+
+License
+-------
+
+Copyright 2013 by John Etchemendy, Dave Barker-Plummer, and Richard Zach
+
+This work may be distributed and/or modified under the
+conditions of the LaTeX Project Public License, either version 1.3
+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.3 or later is part of all distributions of LaTeX
+version 2005/12/01 or later.
+
+This work has the LPPL maintenance status `maintained'.
+
+The Current Maintainer of this work is Richard Zach.
+
+This work consists of the files lplfitch.dtx and lplfitch.ins
+and the derived files lplfitch.sty and lplfitch.pdf.
+
+Versions
+--------
+
+0.9 (2013/05/16) First public beta
+
diff --git a/Master/texmf-dist/doc/latex/lplfitch/lplfitch.pdf b/Master/texmf-dist/doc/latex/lplfitch/lplfitch.pdf
new file mode 100644
index 00000000000..58a7f7ac174
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/lplfitch/lplfitch.pdf
diff --git a/Master/texmf-dist/source/latex/lplfitch/lplfitch.dtx b/Master/texmf-dist/source/latex/lplfitch/lplfitch.dtx
new file mode 100644
index 00000000000..e0f8bb4741e
--- /dev/null
+++ b/Master/texmf-dist/source/latex/lplfitch/lplfitch.dtx
@@ -0,0 +1,796 @@
+% \iffalse meta-comment
+%
+% Copyright (C) 2013 by John Etchemendy, Dave Barker-Plummer, 
+% and Richard Zach
+% -------------------------------------------------------
+% 
+% This work may be distributed and/or modified under the
+% conditions of the LaTeX Project Public License, either version 1.3
+% 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.3 or later is part of all distributions of LaTeX
+% version 2005/12/01 or later.
+%
+% \fi
+%
+% \iffalse
+%<*driver>
+\ProvidesFile{lplfitch.dtx}
+%</driver>
+%<package>\NeedsTeXFormat{LaTeX2e}[1999/12/01]
+%<package>\ProvidesPackage{lplfitch}
+%<*package>
+    [2013/05/16 v0.9 LPL Fitch style]
+%</package>
+%
+%<*driver>
+\documentclass{ltxdoc}
+\usepackage{lplfitch}[2013/05/16]
+\usepackage{hyperref}
+\EnableCrossrefs         
+\CodelineIndex
+\RecordChanges
+\begin{document}
+  \DocInput{lplfitch.dtx}
+  \PrintChanges
+  \PrintIndex
+\end{document}
+%</driver>
+% \fi
+%
+% \CheckSum{0}
+%
+% \CharacterTable
+%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+%   Digits        \0\1\2\3\4\5\6\7\8\9
+%   Exclamation   \!     Double quote  \"     Hash (number) \#
+%   Dollar        \$     Percent       \%     Ampersand     \&
+%   Acute accent  \'     Left paren    \(     Right paren   \)
+%   Asterisk      \*     Plus          \+     Comma         \,
+%   Minus         \-     Point         \.     Solidus       \/
+%   Colon         \:     Semicolon     \;     Less than     \<
+%   Equals        \=     Greater than  \>     Question mark \?
+%   Commercial at \@     Left bracket  \[     Backslash     \\
+%   Right bracket \]     Circumflex    \^     Underscore    \_
+%   Grave accent  \`     Left brace    \{     Vertical bar  \|
+%   Right brace   \}     Tilde         \~}
+%
+%
+% \changes{v0.1}{Aeons ago}{Initial version}
+% \changes{v0.9}{2012/05/16}{First public beta}
+%
+% \GetFileInfo{lplfitch.dtx}
+%
+% \DoNotIndex{\newcommand,\newenvironment}
+%
+% \title{The \textsf{lplfitch} package\thanks{This document
+%   corresponds to \textsf{lplproof}~\fileversion, dated \filedate.}}
+% \author{John Etchemendy \and Dave Barker-Plummer \and Richard Zach}
+%
+% \maketitle
+%
+% \section{Introduction}
+%
+% The package |lplfitch| provides macros for typesetting natural
+% deduction proofs in ``Fitch'' style, with subproofs indented and
+% offset by scope lines.  It produces proofs in the format used in the
+% textbook \href{http://lpl.stanford.edu/}{\textit{Language, Proof,
+% and Logic}} by Dave Barker-Plummer, Jon Barwise, and John
+% Etchemendy.  The package was originally written by John
+% Etchemendy. The current version incorporates changes by Dave
+% Barker-Plummer and Richard Zach.
+%
+% \section{Fitch Proofs by Example}
+% \label{sect:proofs-by-example}
+%
+% In this section we will describe how to typeset the Fitch-style
+% natural deduction proof shown in figure~\ref{fig:example-proof}.
+% This proof uses all of the macros that we have developed for
+% typesetting proofs and therefore serves as a good illustration.
+%
+% \begin{figure}
+% \fitchprf{}{
+%     \subproof{\pline[1.]{\uni{x}{(Cube(x)\lif Small(x))}}}{
+%         \subproof{\pline[2.]{\exi{x}{Cube(x)}}}{
+%             \boxedsubproof[3.]{a}{Cube(a)}{
+%                 \pline[4.]{Cube(a)\lif Small(a)}[\lalle{1}]\\
+%                 \pline[5.]{Small(a)}[\life{4}{3}]\\
+%                 \pline[6.]{\exi{x}{Small(x)}}[\lexii{5}]
+%             }
+%             \pline[7.]{\exi{x}{Small(x)}}[\lexie{2}{3--6}]
+%         }
+%         \pline[8.]{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}[\lifi{2--7}]
+%     }
+%     \pline[9.]{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
+%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}[\lifi{1--8}] 
+% }
+% \caption{An Example Proof}
+% \label{fig:example-proof}
+% \end{figure}
+%
+% The commands for producing this proof are given in
+% figure~\ref{fig:proof-eg-cmds}.  This proof is a little hard to take
+% in all at once, and so in the remainder of this section we will
+% describe the development of this proof, which we hope is of use to
+% readers.
+%
+%\begin{figure}
+%\begin{verbatim}
+% \fitchprf{}{
+%     \subproof{\pline[1.]{\uni{x}{(Cube(x)\lif Small(x))}}}{
+%         \subproof{\pline[2.]{\exi{x}{Cube(x)}}}{
+%             \boxedsubproof[3.]{a}{Cube(a)}{
+%                 \pline[4.]{Cube(a)\lif Small(a)}[\lalle{1}]\\
+%                 \pline[5.]{Small(a)}[\life{4}{3}]\\
+%                 \pline[6.]{\exi{x}{Small(x)}}[\lexii{5}]
+%             }
+%             \pline[7.]{\exi{x}{Small(x)}}[\lexie{2}{3--6}]
+%         }
+%         \pline[8.]{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}[\lifi{2--7}]
+%     }
+%     \pline[9.]{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
+%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}[\lifi{1--8}] 
+% }
+% \end{verbatim}
+% \caption{The commands for producing the proof of
+% figure~\ref{fig:example-proof}}
+% \label{fig:proof-eg-cmds}
+% \end{figure}
+%
+% We recommend developing the commands to typeset a proof from the
+% inside out, starting with the most deeply nested subproof.  We also
+% recommend ignoring justifications until the proof is complete,
+% primarily for simplicity but also because the line numbers are not
+% known until the complete proof structure is present.
+%
+% We begin by writing the lines of the innermost subproof (lines 3--6
+% of the main proof).
+%
+% \begin{quote}
+% \begin{tabular}{ll}
+% |\pline{Cube(a)}| & \formula{Cube(a)}\\
+% |\pline{Cube(a)\lif Small(a)}| & \formula{Cube(a)\lif Small(a)}\\
+% |\pline{Small(a)}| & \formula{Small(a)}\\
+% |\pline{\exi{x}{Small(x)}}| & \formula{\exi{x}{Small(x)}}
+% \end{tabular}
+% \end{quote}
+%
+% The macro |\pline| produces a single line of the proof.  The
+% mandatory argument to |\pline| is the formula to appear within the
+% step.  You will notice that we have used the macro |\lif| to produce
+% an conditional arrow, and |\exi| to produce an existentially
+% quantified formula.  These are members of a suite of macros that we
+% find convenient for producing formulae.  These are described in
+% section~\ref{sect:formulae}.
+%
+% The |\pline| macro may only be used inside a proof context.  We
+% construct such a context by using the |\fitchprf| macro.  This macro
+% has two mandatory arguments, corresponding to the premises and the
+% body of the proof.  Each argument is a list of lines, separated by a
+% newline (|\\|) command.  We therefore embed the lines of our example
+% proof like this:
+%
+% \begin{verbatim}
+% \fitchprf{\pline{Cube(a)}}{
+%     \pline{Cube(a) \lif Small(a)}\\
+%     \pline{Small(a)}\\
+%     \pline{\exi{x}{Small(x)}}
+% }\end{verbatim}
+%
+% Typesetting a document containing this command results in
+% the proof:
+% \begin{quote}
+% \fitchprf{\pline{Cube(a)}}{
+%     \pline{Cube(a) \lif Small(a)}\\
+%     \pline{Small(a)}\\
+%     \pline{\exi{x}{Small(x)}}
+% }
+% \end{quote}
+%
+% Our next step is to embed this proof as a subproof within the larger
+% proof.  This is simply achieved.  We first change the use of
+% |\fitchprf| to a |\subproof| command, and then treat this as a line
+% of the body of another |\fitchprf| command.  The result of doing
+% this is:
+%
+% \begin{verbatim}
+% \fitchprf{\pline{\exi{x}{Cube(x)}}}{
+%     \subproof{\pline{Cube(a)}}{
+%         \pline{Cube(a)\lif Small(a)}\\
+%         \pline{Small(a)}\\
+%         \pline{\exi{x}{Small(x)}}
+%     }
+%     \pline{\exi{x}{Small(x)}}
+% }\end{verbatim}
+%
+% \noindent which yields the proof:
+%
+% \begin{quote}
+% \fitchprf{\pline{\exi{x}{Cube(x)}}}{
+%     \subproof{\pline{Cube(a)}}{
+%         \pline{Cube(a)\lif Small(a)}\\
+%         \pline{Small(a)}\\
+%         \pline{\exi{x}{Small(x)}}
+%     }
+%     \pline{\exi{x}{Small(x)}}
+% }
+% \end{quote}
+%
+% \noindent The new outer |\fitchprf| has two elements in the second
+% argument, one of which is the subproof that we just wrote and the
+% second is a formula.  As we embedded the subproof in the body of the
+% main proof we changed the command from |\fitchprf| to |\subproof|,
+% the definitions of these two macros are almost identical but for the
+% adjustment of vertical spacing after the use of a |\subproof|
+% command.  Note that no |\\| command is required after the use of a
+% |\subproof| command.
+%
+% Two further applications of this technique give us the command:
+%
+% \begin{verbatim}
+% \fitchprf{}{
+%     \subproof{\pline{\uni{x}{(Cube(x)\lif Small(x))}}}{
+%         \subproof{\pline{\exi{x}{Cube(x)}}}{
+%             \subproof{\pline{Cube(a)}}{
+%                 \pline{Cube(a)\lif Small(a)}\\
+%                 \pline{Small(a)}\\
+%                 \pline{\exi{x}{Small(x)}}
+%             }
+%             \pline{\exi{x}{Small(x)}}
+%         }
+%         \pline{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}
+%     }
+%     \pline{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
+%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}
+% }
+% \end{verbatim}
+%
+% \noindent which produces the proof
+%
+% \begin{quote}
+% \fitchprf{}{
+%     \subproof{\pline{\uni{x}{(Cube(x)\lif Small(x))}}}{
+%         \subproof{\pline{\exi{x}{Cube(x)}}}{
+%             \subproof{\pline{Cube(a)}}{
+%                 \pline{Cube(a)\lif Small(a)}\\
+%                 \pline{Small(a)}\\
+%                 \pline{\exi{x}{Small(x)}}
+%             }
+%             \pline{\exi{x}{Small(x)}}
+%         }
+%         \pline{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}
+%     }
+%     \pline{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
+%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}
+% }
+% \end{quote}
+%
+% Notice that the last line contains a long formula, and we have used
+% the |\brokenform| command to typeset this formula.  The
+% |\brokenform| command takes two arguments, the first is the first
+% part of the formula, which will be typeset left justified in the
+% space available, while the second argument contains the remaining
+% pieces of the formula which will appear in subsequent lines.  These
+% lines should be separated by uses of the |\\| command, and each line
+% should (usually) be a |\formula|.  These lines will be typeset right
+% justified in the available space.
+%
+% \subsection{Adding Line Numbers}
+%
+% The |\pline| command takes an optional argument which is the number
+% of the line within the proof.  We can simply add these now that we
+% have all of the lines of the proof.
+%
+% \begin{verbatim}
+% \fitchprf{}{
+%     \subproof{\pline[1.]{\uni{x}{(Cube(x)\lif Small(x))}}}{
+%         \subproof{\pline[2.]{\exi{x}{Cube(x)}}}{
+%             \subproof{\pline[3.]{Cube(a)}}{
+%                 \pline[4.]{Cube(a)\lif Small(a)}\\
+%                 \pline[5.]{Small(a)}\\
+%                 \pline[6.]{\exi{x}{Small(x)}}
+%             }
+%             \pline[7.]{\exi{x}{Small(x)}}
+%         }
+%         \pline[8.]{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}
+%     }
+%     \pline[9.]{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
+%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}
+% }\end{verbatim}
+% \noindent which results in the proof:
+% \begin{quote}
+% \fitchprf{}{
+%     \subproof{\pline[1.]{\uni{x}{(Cube(x)\lif Small(x))}}}{
+%         \subproof{\pline[2.]{\exi{x}{Cube(x)}}}{
+%             \subproof{\pline[3.]{Cube(a)}}{
+%                 \pline[4.]{Cube(a)\lif Small(a)}\\
+%                 \pline[5.]{Small(a)}\\
+%                 \pline[6.]{\exi{x}{Small(x)}}
+%             }
+%             \pline[7.]{\exi{x}{Small(x)}}
+%         }
+%         \pline[8.]{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}
+%     }
+%     \pline[9.]{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
+%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}
+% }
+% \end{quote}
+%
+% In the eventual proof, a boxed constant is introduced at line~3.  We
+% can convert the simple subproof into a boxed subproof.  We use the
+% |\boxedsubproof| macro to achieve this.  The conversion is
+% straightforward, we replace the first argument of the |\subproof|
+% command which was |{\pline[3.]{Cube(a)}}}| by the three arguments
+% |[3.]{a}{Cube(a)}| obtaining
+%
+% \begin{verbatim}
+% \boxedsubproof[3.]{a}{Cube(a)}{
+%     \pline[4.]{Cube(a)\lif Small(a)}\\
+%     \pline[5.]{Small(a)}\\
+%     \pline[6.]{\exi{x}{Small(x)}}
+% }\end{verbatim}
+%
+% \subsection{Adding Justifications}
+%
+% The final thing that we need to do to complete the desired proof is
+% the addition of justifications.  To produce a justified line we need
+% to then add the optional justification argument.
+%
+% \begin{verbatim}\pline[5.]{Small(a)}[\ife{4}{3}]\end{verbatim}
+%
+% \noindent The \verb|\ife| macro produces a justification using the
+% $\lif$-elimination rule of the logic.  This is one of a suite of
+% macros that we developed to produce justifications in a uniform
+% manner.  These are described in section~\ref{sect:justifications}.
+%
+% \subsection{Command Reference}
+% 
+% The |\pline| command can be used to typeset proof lines. It takes
+% the formula as a mandatory argument, and line number and
+% justification as optional arguments: |\pline|\oarg{line
+% number}\marg{formula}\oarg{justification}.  The variant |\fpline|
+% works the same, except it produces a focus slider.  In case you want
+% to typeset a line in an argument or proof that is not typeset as a
+% formula (e.g., plain text), use the |\tline| command. It takes a
+% line number as optional argument.
+%
+% \subsection{Obsolete Commands}
+%
+% The original version of |lplfitch| set lines of proofs using two
+% separate macros, the |\nline| and |\jline| commands.  They are
+% superceded by the |\pline| command and are included for backward
+% compatibility only.
+%
+% A numbered line is produced by |\nline|, with the optional argument
+% the line number.  A justified line is produced using the
+% \verb|\jline| macro, which has one mandatory and one optional
+% argument.  The optional argument contains the justification, while
+% the mandatory argument must contain {\em all} of the arguments
+% previously given to \verb|\nline|.  So the command
+%
+% \begin{verbatim}\nline[5.]{Small(a)}\end{verbatim}
+% 
+% \noindent produces exactly the same output as
+%
+% \begin{verbatim}\jline{[5.]{Small(a)}}\end{verbatim}
+% 
+% \noindent but notice that both the arguments to \verb|\nline| are
+% passed within the single argument to \verb|\jline|. To produce a
+% justified line using |\jline|, you would also include the
+% justification as an optional argument, say,
+%
+% \begin{verbatim}\jline{[5.]{Small(a)}}[\life{2}{3}]\end{verbatim}
+%
+% \section{Logical Formulae}
+% \label{sect:formulae}
+%
+% We set our formulae using sans-serif font and we also need to be in
+% math mode because the use of logical connectives.  The
+% \verb|\formula| command takes a formula to set as its argument, and
+% handles both font and mode change.  If the LPL convention of sans-serif
+% formulas is not desired, you can simly redefine |\formula| as
+% \begin{verbatim}\renewcommand{\formula}[1]{\ensuremath{#1}}\end{verbatim}
+%
+% Many of the commands that follow require that they are used in a
+% formula, or math, context.
+%
+% \subsection{Connectives}
+%
+% We introduce our own (usually) shorter names for logical
+% connectives.  All of these commands require a formula context.
+%
+% \begin{center}
+% \begin{tabular}{lc}
+% \bf Usage & \bf Output\\
+% \hline\\
+% \verb|\land| & \formula{\land}\\
+% \verb|\lor| & \formula{\lor}\\
+% \verb|\lif| & \formula{\lif}\\
+% \verb|\liff| & \formula{\liff}\\
+% \verb|\lnot| & \formula{\lnot}\\
+% \verb|\lfalse| & \formula{\lfalse}\\
+% \verb|\lall| & \formula{\lall}\\
+% \verb|\lis| & \formula{\lis}
+% \end{tabular}
+% \end{center}
+%
+% \subsection{Quantified Formulae}
+%
+% So that we don't have to think about spacing when setting quantified
+% formulae, we defined the commands |\exi| and |\uni|.  Use
+% |\exi{x}{P(x)}| to obtain \formula{\exi{x}{P(x)}}, and
+% |\uni{x}{\exi{y}{(P(x)\lif Q(x,y))}}| for
+% \formula{\uni{x}{\exi{y}{(P(x)\lif Q(x,y))}}}, for example.  |\exi|
+% and |\uni| require a formula context.
+%
+% \section{Justifications}
+% \label{sect:justifications}
+%
+% Here are the macros that we have developed to typeset justifications
+% within a proof.  These do not require a formula context.
+%
+% \begin{center}
+% \begin{tabular}{ll}
+% \bf Usage & \bf Output\\
+% \hline\\
+% |\landi{2, 3}| &\landi{2, 3}\\
+% |\lande{4}|&\lande{4}\\
+% |\lori{5}| & \lori{5}\\
+% |\lore{6}{7--9}{11--13}| &\lore{6}{7--9}{11--13}\\
+% |\lnoti{14--15}| &\lnoti{14-15}\\
+% |\lnote{16}| &\lnote{16}\\
+% |\lfalsei{17}{19}| &\lfalsei{17}{19}\\
+% |\lfalsee{20}|&\lfalsee{20}\\
+% |\lifi{21--25}| &\lifi{21--25}\\
+% |\life{27}{30}| &\life{27}{30}\\
+% |\liffi{33--37}{40-50}|&\liffi{33--37}{40--50}\\
+% |\liffe{55}{57}| &\liffe{55}{57}\\
+% |\reit{4}|&\reit{4}\\
+% |\eqi| &\eqi\\
+% |\eqe{7}{11}|&\eqe{7}{11}\\
+% |\lalli{9--12}|&\lalli{9--12}\\
+% |\lalle{13}|&\lalle{13}\\
+% |\lexii{15}| &\lexii{15}\\
+% |\lexie{17}{18-30}| &\lexie{17}{18--30}\\
+% \end{tabular}
+% \end{center}
+%
+% \section{Other Macros}
+% \label{sect:other-macros}
+%
+% \subsection{Arguments}
+%
+% When you want to typeset an argument, for example when setting an
+% exercise requiring the proof of some conclusion from a collection of
+% premises, you should use the |\fitcharg| command.  This command
+% takes two arguments, both mandatory, the premise lines which are set
+% above the Fitch bar, and the conclusion lines, which go below.
+% Here's an example.  The argument
+%
+%\begin{quote}
+%  \fitcharg{\formula{P(a)}\\ \formula{Q(a)}}{\formula{S(a)}}
+%\end{quote}
+%
+%\noindent is typeset by the command:
+%\begin{verbatim}\fitcharg{
+%     \formula{P(a)}\\ 
+%     \formula{Q(a)}
+% }{
+%     \formula{S(a)}
+% }\end{verbatim}
+% \noindent Notice that multiple lines are separated by a use of the
+% \LaTeX\ command |\\|.
+%
+% \subsection{Fitch Contexts}
+%
+% The |\fitchctx| command is used for setting proof fragments which do
+% not include the horizontal Fitch bar.  We use these, for example,
+% when formally describing the inference rules of our logic.  The
+% command below, for example, typesets our description of the rule of
+% conditional proof.
+%
+% Notice here that we use the command |\ellipsesline| to produce a
+% line of the ``proof'' containing a vertical ellipses (using the
+% |\pline{\vdots}| results in the ellipses not being centered on the
+% line).
+%
+% Another new feature of this situation is the use of the |\fpline|
+% command.  This command works just like the |\pline| command and
+% produces exactly what the |\pline| command would, except that a
+% focus slider appears to the left of the Fitch bar in question.  The
+% |\fpline| command does not work in the argument lines of
+% |\fitchprf|  or |\fitcharg|.
+%
+% \begin{verbatim}
+% \fitchctx{
+%     \subproof{\pline[$n$.]{P}}{
+%         \ellipsesline\\
+%         \pline[$m$.]{Q}
+%     }
+%     \fpline{P \lif Q}[\lifi{$n$--$m$}]
+% }
+% \end{verbatim}
+%
+% \begin{quote}
+% \fitchctx{
+%     \subproof{\pline[$n$.]{P}}{
+%         \ellipsesline\\
+%         \pline[$m$.]{Q}
+%     }
+%     \fpline{P \lif Q}[\lifi{$n$--$m$}]
+% }
+% \end{quote}
+%
+% \section{Other Packages}
+%
+% Two other \LaTeX{} packages provide functionality to typeset
+% Fitch-style proofs. They differ from |lplfitch| in that they set the
+% line numbers close to the left edge of the proof, while |lplfitch|
+% sets them close to the formula.  Another difference is that subroofs
+% can easily be copied and work the same regardless of the depth of
+% nesting.
+%
+% Peter Selinger's package is
+% available at
+%\begin{quote}
+% \href{http://www.mathstat.dal.ca/~selinger/fitch/}{|http://www.mathstat.dal.ca/\~{
+% }selinger/fitch/|},
+% \end{quote}
+% and that by Johan Kl\"uwer at
+% \begin{quote}
+% \href{http://folk.uio.no/johanw/FitchSty.html}{|http://folk.uio.no/johanw/FitchSty.html|}.
+% \end{quote}
+%
+% \StopEventually{}
+%
+% \section{Implementation}
+%
+%    \begin{macrocode}
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{lplfitch}[2013/05/07 -- Fitch Proofs a la LPL]
+%    \end{macrocode}
+%
+% \begin{macro}{\formula}
+% Typesets a formula (in math mode, letters typeset in sans-serif as in LPL
+%    \begin{macrocode}
+\newcommand*{\formula}[1]{\ensuremath{\sf{#1}}}
+%    \end{macrocode}
+% \end{macro}
+%
+% \subsection{Connectives and Quantifiers}
+% We provide convenient and short commands for logical symbols.
+%    \begin{macrocode}
+\newcommand*\lif{\rightarrow}
+\newcommand*\liff{\leftrightarrow}
+\newcommand*\lfalse{\bot}
+\newcommand*\lall{\forall}
+\newcommand*\lis{\exists}
+%    \end{macrocode}
+% The following provide for commands for setting quantified formulae, inserting correct space
+% between variable and formula.  It can be redifined using |\renewcommand| if you want to use them but
+% want quantifiers set differently (e.g., with parentheses)
+%    \begin{macrocode}
+\newcommand*{\quant}[3]{#1 #2\;#3}
+\newcommand*{\exi}[2]{\quant{\lis}{#1}{#2}}
+\newcommand*{\uni}[2]{\quant{\lall}{#1}{#2}}
+%    \end{macrocode}
+% \subsection{Justifications}
+%
+% The folowing commands are used to generate justifications, e.g.,
+% |\landi{1, 2}| produces ``\landi{1, 2}''.
+%    \begin{macrocode}
+\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}
+%    \end{macrocode}
+%
+% \subsection{Dimensions}
+%
+% The following dimensions can be redefined with |\setlength|
+%
+% \begin{macro}{\fitchargwidth}
+% Width of formulas in arguments
+%    \begin{macrocode}
+\newlength{\fitchargwidth}  
+\setlength{\fitchargwidth}{3.5in}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\fitchprfwidth}
+% Width of formulas in proofs
+%    \begin{macrocode}
+\newlength{\fitchprfwidth}
+\setlength{\fitchprfwidth}{3.0in}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\fitchctxwidth}
+% Width of formulas in Fitch contexts
+%    \begin{macrocode}
+\newlength{\fitchctxwidth}  
+\setlength{\fitchctxwidth}{1in}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\fitchsep}
+% Distance between scope line and formula
+%    \begin{macrocode}
+\newlength{\fitchsep}   
+\setlength{\fitchsep}{10pt}
+%    \end{macrocode}
+% \end{macro}
+%
+% \subsection{Contexts, Arguments, Proofs}
+%
+% \begin{macro}{\fitchctx} Typesets a Fitch context, e.g., specification of 
+% a rule, in which a focus slider is typeset to the left of the conclusion 
+%    \begin{macrocode} 
+\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%
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\fitchprf} Typesets a fitch proof
+%    \begin{macrocode}
+\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%
+}
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\fitcharg} Typesets an argument (without line
+% numbers). Takes two arguments, the premises and conclusion lines of
+% the argument.
+%    \begin{macrocode}
+\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}
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\slider} Typesets the focus arrow.
+%    \begin{macrocode}
+\newcommand*{\slider}{\mbox{$\triangleright \;$}}
+%    \end{macrocode}
+% \end{macro}
+% 
+% \begin{macro}{\pline} Typesets a proof line with an optional line
+% number (before the formula argument) and an optional justification
+% (after the formula argument)
+%    \begin{macrocode}
+\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} 
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\fpline} Like |pline| except produces a focus slider
+% on the left
+%    \begin{macrocode}
+\newcommand*\fpline{\slider\pline} 
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\tline} Typesets proof line containing text with an
+% optional line number.
+%    \begin{macrocode}
+\newcommand*{\tline}[2][{}]{ & #1\hspace{.6em}{#2}}
+%    \end{macrocode}
+% \end{macro}
+%
+% The following macros |\nline|, |\jline|, and |\fline|
+% are the commands provided in the original version
+% of |lplfitch| and are included for backwards compatibility. 
+%    \begin{macrocode}
+\newcommand*{\nline}[2][{}]{ & #1\formula{\;#2}}
+%    \end{macrocode}
+% justified line (justification optional)
+% |\jline[justification]{args for line}|
+%    \begin{macrocode}
+\newcommand*{\jline}[2][{}]{\nline#2 & #1}
+%    \end{macrocode}
+% focused line
+%    \begin{macrocode}
+\newcommand*{\fline}[1]{\slider \jline#1}
+%    \end{macrocode}
+%
+% \begin{macro}{\ellipsesline}
+% Producing vertical ellipses in a line on their own.
+% This takes care of centering the ellipses in their line.
+%    \begin{macrocode}
+\newcommand*{\ellipsesline}[0]{\nline{\;\raise.65ex\hbox{\vdots}}}
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\subproof}
+% This command sets a subproof within a proof.
+% The arguments are the line before, and the lines after
+% the horizontal fitch bar.
+%    \begin{macrocode}
+\newcommand{\subproof}[2]{&\fitchprf{#1}{#2}\\}
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\boxedsubproof}
+% Produces a new boxed subproof.
+% |\boxedsubproof|\oarg{n}\marg{c}\marg{premise}\marg{body}, where
+% \meta{n} is the number of the premise line, \meta{c} is the
+% constant(s) to be boxed, \meta{premise} is the premise of the
+% subproof, and \meta{body} contains the lines of the subproof.
+%    \begin{macrocode}
+\newcommand{\boxedsubproof}[4][{}]{
+     \subproof{\nline[#1]{\fbox{\formula{#2}}\;#3}}{#4}
+}
+%    \end{macrocode}
+% \end{macro}
+% \begin{macro}{\brokenform}
+% A crude attempt at dealing with a formula which need to be broken to
+% fit in the proof.  We take two arguments, the first line of the
+% formula which is left justified, and the remainder of the lines,
+% which are right justified.  The first argument is set as a
+% |\formula| but the second is not (as it may contain line breaks
+% itself).
+%    \begin{macrocode}
+\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
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \Finale
+\endinput
diff --git a/Master/texmf-dist/source/latex/lplfitch/lplfitch.ins b/Master/texmf-dist/source/latex/lplfitch/lplfitch.ins
new file mode 100644
index 00000000000..5de9a57126c
--- /dev/null
+++ b/Master/texmf-dist/source/latex/lplfitch/lplfitch.ins
@@ -0,0 +1,59 @@
+%%
+%% Copyright (C) 2013 by 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.
+%%
+
+\input docstrip.tex
+\keepsilent
+
+\usedir{tex/latex/lplfitch}
+
+\preamble
+
+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.
+
+\endpreamble
+
+\generate{\file{lplfitch.sty}{\from{lplfitch.dtx}{package}}}
+
+\obeyspaces
+\Msg{*************************************************************}
+\Msg{*                                                           *}
+\Msg{* To finish the installation you have to move the following *}
+\Msg{* file into a directory searched by TeX:                    *}
+\Msg{*                                                           *}
+\Msg{*     lplfitch.sty                                          *}
+\Msg{*                                                           *}
+\Msg{* To produce the documentation, do                          *}
+\Msg{*                                                           *}
+\Msg{*     pdflatex lplfitch.dtx                                 *}
+\Msg{*     makeindex -s gglo.ist -o lplfitch.gls lplfitch.glo    *}
+\Msg{*     pdflatex lplfitch.dtx                                 *}
+\Msg{*     pdflatex lplfitch.dtx                                 *}
+\Msg{*                                                           *}
+\Msg{* Happy TeXing!                                             *}
+\Msg{*                                                           *}
+\Msg{*************************************************************}
+
+\endbatchfile
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'.
diff --git a/Master/tlpkg/bin/tlpkg-ctan-check b/Master/tlpkg/bin/tlpkg-ctan-check
index ffc64cf8612..94e952982af 100755
--- a/Master/tlpkg/bin/tlpkg-ctan-check
+++ b/Master/tlpkg/bin/tlpkg-ctan-check
@@ -272,7 +272,7 @@ my @TLP_working = qw(
     listbib listing listings listings-ext listliketab listofsymbols
     lithuanian liturg lkproof lm lm-math lmake
     locality localloc logbox logical-markup-utils logicpuzzle logpap logreq
-    longnamefilelist loops lpic lps lsc
+    longnamefilelist loops lpic lplfitch lps lsc
     lshort-bulgarian lshort-chinese lshort-czech lshort-dutch lshort-english
     lshort-finnish lshort-french lshort-german lshort-italian
     lshort-japanese lshort-korean lshort-mongol lshort-persian
diff --git a/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc b/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc
index 0932966fb4f..9e74d6d7072 100644
--- a/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc
+++ b/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc
@@ -23,6 +23,7 @@ depend faktor
 depend interval
 depend ionumbers
 depend isomath
+depend lplfitch
 depend mathcomp
 depend mattens
 depend mhequ
diff --git a/Master/tlpkg/tlpsrc/lplfitch.tlpsrc b/Master/tlpkg/tlpsrc/lplfitch.tlpsrc
new file mode 100644
index 00000000000..e69de29bb2d
--- /dev/null
+++ b/Master/tlpkg/tlpsrc/lplfitch.tlpsrc