trunk/Master/texmf-dist/source/latex/flagderiv

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

2 files changed, 1324 insertions, 0 deletions

diff --git a/Master/texmf-dist/source/latex/flagderiv/flagderiv.dtx b/Master/texmf-dist/source/latex/flagderiv/flagderiv.dtx
new file mode 100644
index 00000000000..c9025c73e2e
--- /dev/null
+++ b/Master/texmf-dist/source/latex/flagderiv/flagderiv.dtx
@@ -0,0 +1,1261 @@
+% \iffalse meta-comment
+%
+% Copyright (C) 2005 by Paul van Tilburg <paul@luon.net>
+% ------------------------------------------------------
+% 
+% This package is free software; you can redistribute it and/or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation; either version 2 of the License, or
+% (at your option) any later version.
+% 
+% This package is distributed in the hope that it will be useful,
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+% GNU General Public License for more details.
+% 
+% You should have received a copy of the GNU General Public License
+% along with this package; if not, write to the Free Software
+% Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.%
+%
+% \fi
+%
+% \iffalse
+%<*driver>
+\ProvidesFile{flagderiv.dtx}
+%</driver>
+%<flagderiv>\NeedsTeXFormat{LaTeX2e}[1999/12/01]
+%<flagderiv>\ProvidesPackage{flagderiv}
+%<*flagderiv>
+    [2005/08/26 v0.10 Flag style derivation package]
+%</flagderiv>
+%
+%<*driver>
+\documentclass{ltxdoc}
+
+\usepackage{amsmath, amssymb}
+\usepackage{calc}
+\usepackage{flagderiv}
+\usepackage{fvrb-ex}
+\usepackage{theorem}
+\usepackage{url}
+
+\setlength{\parindent}{0pt}
+\setlength{\parskip}{\medskipamount}
+\setcounter{tocdepth}{2}
+
+\theoremstyle{plain}
+\newtheorem{lemma}{Lemma}
+\newcommand{\false}{\textit{False}}
+\newcommand{\flags}{\texttt{flagderiv}}
+\newcommand{\IHbase}{\underline{\textit{Base}}:~}
+\newcommand{\IHhyp}{\underline{\textit{Induction-hypothesis}}:~}
+\newcommand{\IHstep}{\underline{\textit{Step}}:~}
+\newcommand{\Nat}{\ensuremath{\mathbb{N}}}
+\newcommand{\All}{\ensuremath{\mathbb{Z}}}
+\newcommand{\Powerset}{\ensuremath{\mathcal{P}}}
+
+\renewcommand{\implies}{\Rightarrow}
+\newcommand{\biimplies}{\Leftrightarrow}
+\newcommand{\OHA}{\rightarrow}
+\newcommand{\THA}{\twoheadrightarrow}
+\newcommand{\NHA}[1]{\stackrel{#1}{\rightarrow}}
+\newcommand{\CRtext}{\ensuremath{\mathit{CR}}}
+\newcommand{\CR}{\ensuremath{(\forall a, b, c\in A: a\THA b\land a\THA c:%
+                             (\exists d\in A:: b\THA d\land c\THA d))}}
+\newcommand{\MCtext}{\ensuremath{\mathit{mixed~confluent}}}
+\newcommand{\MC}{\ensuremath{(\forall a, b, c\in A: a\OHA b\land a\THA c:%
+                             (\exists d\in A:: b\THA d\land c\THA d))}}
+
+\EnableCrossrefs         
+\CodelineIndex
+\RecordChanges
+
+\begin{document}
+  \DocInput{flagderiv.dtx}
+\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.9f}{2005/02/04}{Initial version.}
+% \changes{v0.9g}{2005/05/16}{Added example and usage documentation.}
+% \changes{v0.9h}{2005/06/06}{Added the flagderiv* environment.}
+% \changes{v0.9i}{2005/06/10}{Fixed minor issues in the documentation
+%                        and resolved a ref-format bug.}
+% \changes{v0.10}{2005/08/26}{Drop dependancy on farray, include fix.}
+%
+% \GetFileInfo{flagderiv.dtx}
+%
+% \DoNotIndex{\newcommand,\newenvironment}
+% 
+% \title{The \textsf{flagderiv} package\thanks{This document
+%   corresponds to \textsf{flagderiv}~\fileversion, dated \filedate.}}
+% \author{Paul van Tilburg \\ \url{paul@luon.net}}
+%
+% \maketitle
+%
+% \tableofcontents
+%
+% \section{Introduction}
+%
+%  This document describes how to use \flags~to make flag-style proofs in
+%  \LaTeX.
+%
+%  It can handle taking steps, making assumptions, introducing variables and
+%  conclusions.  The package allows the style to be configured.  For
+%  example, the variable introduction symbol can be redefined.  Other
+%  features include multiple page flag-style proofs.
+%
+%  The documentation and all examples are based upon version \fileversion\ 
+%  of \flags.
+%
+%  \begin{center}
+%   \scriptsize
+%     \renewcommand{\introsymb}{\text{Let}}
+%     \begin{flagderiv}
+%      \assume{i:assume:no-package}{\text{There is no nice package to do flag-style proofs}}{}
+%       \introduce{i:intro:feature}{x\text{, such that } x\text{ is a flag-style feature}}{}
+%        \skipsteps{5}{\vdots}{}
+%        \step{i:feature-met}{\flags~\text{can do it}}{}
+%       \conclude{i:conclusion}{\flags~\text{fulfils my every flag-style proof need}}
+%                              {$\forall$-introduction on \ref{i:intro:feature} and \ref{i:feature-met}}
+%       \step{i:false}{\false}{\false-introduction on \ref{i:assume:no-package} and \ref{i:conclusion}}
+%      \conclude{i:conclude:not-no-package}{\lnot (\text{There is no nice package to do flag-style proofs})}
+%                                          {$\lnot$-introduction on \ref{i:assume:no-package} and \ref{i:false}}
+%      \step{i:step:nice-package}{\text{So, there exists a nice package to do flag-style proofs}}
+%                                {$\lnot\lnot$-elimination on \ref{i:conclude:not-no-package}}
+%     \end{flagderiv}
+%  \end{center}
+%
+% \section{Acknowledgements}
+%
+% I want to thank Jan Zwanenburg and Erik Poll for the first versions of
+% this package, professor R.P.\ Nederpelt for his ever-persisting package
+% reviews, feedback and suggestions and last but not least Mark van Eijk,
+% who has written parts of section~\ref{sec:usage} and all examples in
+% section~\ref{sec:ex}.
+%
+% \section{Usage\label{sec:usage}}
+%
+%  This section explains how the \flags\ package works by means of examples 
+%  and how the commands should be used. I try to cover all possibilities and
+%  features of this package. For bigger examples, please refer to
+%  section~\ref{sec:ex}; for more detailed documentation on the commands
+%  and inner workings, refer to the \flags\ package itself.
+% 
+%   \subsection{Basic derivations}
+%    \DescribeEnv{flagderiv}
+%    Basic derivations are written using an intuitive command sequence
+%    placed in the |flagderiv| environment\index{usage}. The example below
+%    uses auto-numbering of the lines. Variable introductions, assumptions, 
+%    steps and conclusions can be done using the following commands 
+%    respectively:
+%
+%    \begin{itemize}
+%     \item \DescribeMacro{\introduce}\index{usage}
+%           |\introduce|\marg{label}\marg{formula}\marg{comment}, 
+%     \item \DescribeMacro{\assume}\index{usage}
+%           |\assume|\marg{label}\marg{formula}\marg{comment},
+%     \item \DescribeMacro{\step}\index{usage}
+%           |\step|\marg{label}\marg{formula}\marg{comment}, and 
+%     \item \DescribeMacro{\conclude}\index{usage}
+%           |\conclude|\oarg{number}\marg{label}\marg{formula}\marg{comment}.
+%    \end{itemize}
+% 
+%    Lines can be referred to using the {\em label} that is provided as the
+%    first argument to each of the commands. {\em Formulas} are placed in
+%    the second argument and a {\em comment} in the third. 
+%    See subsection~\ref{sec:usage:multi} for the explanation of the optional
+%    argument {\em number} of |\conclude|.
+% 
+%    \begin{Example}[gobble=7,frame=single,label=Auto-numbering]
+%      \begin{flagderiv}
+%        \introduce{in-x}{x: \Nat}{Introduction of $x$}
+%          \assume{as-x}{x > 5}{Assumption}
+%            \step{big-x}{x > 1}{Arithmetic on \ref{in-x} and \ref{as-x}}
+%          \conclude{conc}{x > 5 \implies x > 1}
+%                         {$\implies$-intro on \ref{as-x} and \ref{big-x}}
+%        \conclude{}{\forall x \in \Nat: x > 5 \implies x > 1}
+%                   {$\forall$-intro on \ref{in-x} and \ref{conc}}
+%      \end{flagderiv}
+%    \end{Example}
+% 
+%    The following example uses manual numbering. This is done by using the
+%    \DescribeMacro{\introduce*}
+%    starred versions of the previous given commands (|\introduce*|,
+%    \DescribeMacro{\assume*}
+%    \DescribeMacro{\step*}
+%    \DescribeMacro{\conclude*}
+%    |\assume*|, |\step*| and |\conclude*|) and using a
+%    {\em custom number} instead of a {\ em label} as the first argument. 
+%    Note that because of this, derivation line references are not possible
+%    and should be done manually as well.
+% 
+%    \begin{Example}[gobble=7,frame=single,label=Manual numbering]
+%      \begin{flagderiv}
+%        \introduce*{$(1)$}{x: \Nat}{Introduction of $x$}
+%          \assume*{$(2)$}{P(x)}{Assumption}
+%            \skipsteps*{\dots}{}
+%            \step*{$(n - 2)$}{Q(x)}{}
+%          \conclude*{$(n - 1)$}{P(x) \implies Q(x)}
+%                               {$\implies$-intro on $(2)$ and $(n - 2)$}
+%        \conclude*{$(n)$}{\forall x \in \Nat: P(x) \implies Q(x)}
+%                         {$\forall$-intro on $(1)$ and $(n - 1)$}
+%      \end{flagderiv}
+%    \end{Example}
+% 
+%    Note that the |\skipsteps*| used in the previous example is
+%    explained in section~\ref{sec:usage:skipsteps}.
+% 
+%   \subsection{Concluding multiple assumptions/introductions\label{sec:usage:multi}}
+%    Sometimes it is useful to make a conclusion from multiple open
+%    assumptions and/or introductions at once. This can be done by supplying
+%    an optional {\em number} to the |\conclude| command. Usage is
+%    illustrated in the example below.
+% 
+%    \begin{Example}[gobble=7,frame=single,label=Multiple conclusion]
+%      \begin{flagderiv} 
+%        \introduce{}{x: \Nat}{}
+%          \assume{}{P(x)}{}
+%            \step{}{Q(x)}{}
+%        \conclude[2]{}{\forall x \in \Nat: (P(x) \implies Q(x))}{}
+%      \end{flagderiv}
+%    \end{Example}
+% 
+%   \subsection{Skipping steps\label{sec:usage:skipsteps}}
+%    When writing example derivations or abbreviating those where
+%    obvious/trivial steps may be skipped, one can use the
+%    \DescribeMacro{\skipsteps}
+%    |\skipsteps|\marg{number}\marg{formula}\marg{comment} command for
+%    auto-numbered derivations.  This commands takes the {\em number} of
+%    steps to skip as the first argument, a {\em formula} as the second and
+%    a {\em comment} as the third, like a normal step.
+%    \vspace{3em}
+%    
+%    \begin{Example}[gobble=7,frame=single,label=Skipping 5 steps]
+%      \begin{flagderiv}
+%        \assume{as}{P \implies Q}{}
+%          \step{lem-p}{P \lor \neg P}{LEM}
+%          \skipsteps{5}{\dots}
+%                       {Prove $\neg P \lor Q$ for $P$ and $\neg P$}
+%          \step{or-elm}{\neg P \lor Q}{$\lor$-elim on \ref{lem-p}}
+%      \end{flagderiv}
+%    \end{Example}
+% 
+%    For skipping an unknown number of steps in a manual numbered
+%    \DescribeMacro{\skipsteps*}
+%    derivation, the command |\skipsteps*|\marg{formula}\marg{comment} can
+%    be used.  Here the number of steps to skip must be omitted, since there
+%    is no counting involved.  See for example the $\implies$-intro rule:
+% 
+%    \begin{Example}[gobble=7,frame=single,label=Skipping steps]
+%      \begin{flagderiv}
+%        \assume*{$(1)$}{P}{Assumption}
+%          \skipsteps*{\dots}{Derive $Q$}
+%          \step*{$(n - 1)$}{Q}{}
+%        \conclude*{$(n)$}{P \implies Q}
+%                         {$\implies$-intro on $(1)$ to $(n - 1)$}
+%      \end{flagderiv}
+%    \end{Example}
+% 
+%   \subsection{Closing assumptions/introductions}
+%    Assumptions and introductions (contexts) are not always closed by a
+%    conclusion, it is sometimes useful to keep proven propositions within
+%    \DescribeMacro{\done}
+%    its context.  The |\done| command (|\done|\oarg{number}) can be used to
+%    close a assumption and/or introduction without mentioning why.  It takes
+%    an optional argument {\em number} to close multiple open assumptions
+%    and/or introductions.  An example from the WTT (Weak Type Theory):
+% 
+%    \begin{Example}[gobble=7,frame=single,label=Closing assumptions/introductions]
+%      \begin{flagderiv}
+%        \introduce{}{n: \Nat}{}
+%          \introduce{}{d: \Nat}{}
+%            \step{}{\text{$d$ is a divisor of $n$} := 
+%                     \exists_{k: \Nat} (n = d \cdot k)}{}
+%          \done
+%          \introduce{}{m: \Nat}{}
+%            \step{}{\text{$m$ is a multiple of $n$} := 
+%                     \exists_{k: \Nat} (m = k \cdot n)}{}
+%        \done[2]
+%      \end{flagderiv}
+%    \end{Example}
+%
+%    \vspace{-1em}
+%    The last |\done[2]| can be omitted since closing the \flags\ environment
+%    implicitly closes all open introductions and assumptions.
+%
+% 
+%   \subsection{Spacing between lines}
+%    The spacing between derivation lines defaults to {\tt 8pt} but can be 
+%    changed
+%    \DescribeMacro{derivskip}\index{setting}
+%    by adjusting the length (using |\setlength| on {\tt derivskip})
+%    before starting or during a \flags\ environment. See for example the
+%    more condensed proof:
+% 
+%    \begin{Example}[gobble=7,frame=single,label=Condensing a derivation]
+%      \setlength{\derivskip}{4pt}
+%      \begin{flagderiv}
+%        \assume{}{P}{}
+%          \assume{}{Q}{}
+%            \step{}{P}{}
+%          \conclude{}{Q \implies P}{}
+%        \conclude{}{P \implies Q \implies P}{}
+%      \end{flagderiv}
+%    \end{Example}
+% 
+%    Note that flag derivations will automatically be split across pages if
+%    it is too long and the |flagderiv| environment is used.  See also the
+%    {\tt longtable} package.  This does not happen for |flagderiv*|, which
+%    is a normal |tabular|.
+% 
+%   \subsection{The introduction symbol}
+%    \DescribeMacro{\introsymb}\index{changing}
+%    The way an introduction flag differs from an assumption flag is that it
+%    is prefixed with an {\em introduction symbol}. This symbol is by
+%    default set to $\mathbf{var}$ (|\mathbf{var}|) but can be changed
+%    to a different symbol, for example to $\leadsto$ (|\leadsto|) or
+%    just `Let'. This can be changed by redefining the |\introsymb|
+%    command before opening the \flags\ environment.
+% 
+%    \begin{Example}[gobble=7,frame=single,label=Changing the introduction symbol]
+%      \renewcommand{\introsymb}{\textbf{Let}}
+%      \begin{flagderiv}
+%        \introduce{intro-x}{x: \Nat}{Introduction}
+%          \introduce{intro-y}{y: \Nat}{Introduction}
+%            \skipsteps*{\ddots}{}
+%      \end{flagderiv}
+%    \end{Example}
+% 
+%   \subsection{Numbering and format}
+%    When the derivation lines are automatically numbered the numbers are
+%    formatted as ``({\em number})'' and so are the references. This format
+%    \DescribeMacro{fd@stepcount}
+%    \DescribeMacro{\thestepcount}\index{changing}
+%    can be changed by overriding the |\thestepcount| command using the
+%    {\tt fd@stepcount} counter before opening the \flags\ environment.
+% 
+%    \begin{Example}[gobble=7,frame=single,label=Changing the numbering format]
+%      \renewcommand{\thestepcount}{[\Roman{fd@stepcount}]}
+%      \begin{flagderiv}
+%        \step{ass}{P \implies Q}{}
+%        \step{lem}{P \lor \neg P}{LEM}
+%        \assume{ass-nP}{\neg P}{Assumption}
+%          \step{s0}{\neg P \lor \neg Q}{$\lor$-intro on \ref{ass-nP}}
+%        \done
+%        \assume{ass-nnP}{P}{Assumption}
+%          \step{s1}{Q}{$\implies$-elim on \ref{ass-nnP} and \ref{ass}}
+%          \step{s2}{\neg P \lor \neg Q}{$\lor$-intro on \ref{s1}}
+%        \done
+%        \step{or-el}{\neg P \lor Q}
+%                    {$\lor$-elim on \ref{lem}, \ref{s0} and \ref{s2}}
+%      \end{flagderiv}
+%    \end{Example}
+% 
+%    \DescribeMacro{\thesteplabel}\index{changing}
+%    Since the manual numbered derivations use no counter, the format can be
+%    changed by overriding the |\thesteplabel| command which will take
+%    one argument, the {\em custom number}.
+% 
+%    \begin{Example}[gobble=7,frame=single,label=Changing the numbering format]
+%      \renewcommand{\thesteplabel}[1]{#1.}
+%      \begin{flagderiv}
+%        \assume*{1}{P}{Assumption}
+%          \skipsteps*{\dots}{Derive $Q$}
+%          \step*{n - 1}{Q}{}
+%        \conclude*{n}{P \implies Q}{$\implies$-intro on 1 to n - 1}
+%      \end{flagderiv}
+%    \end{Example}
+% 
+%    Note that since references are also manually done, the same format
+%    should be used there by the writer him/herself.
+% 
+%   \subsection{Inline comments}
+%    In general there are two ways to place the comments with respect to
+%    the formulas in derivations. The first is behind the formula (the
+%    default). The second way is to place them inline, that is, on a separate 
+%    line before the formula.
+% 
+%    All \flags\ environments can be set globally to display the comments
+%    inline by passing the global option {\tt inlcmnts} to the \flags\
+%    package (e.g.\\|\usepackage[inlcmnts]{flagsderiv}|).
+% 
+%    \DescribeMacro{\inlcmnts}\index{usage}
+%    Giving the |\inlcmnts| command makes the environments after this
+%    command explicitly switch into inline-comment-mode (the default or
+%    \DescribeMacro{\noinlcmnts}\index{usage}
+%    global option is forgotten) after which giving |\noinlcmnts| will set 
+%    it back to normal mode.
+% 
+%    \begin{Example}[gobble=7,frame=single,label=Inline comments]
+%      \inlcmnts
+%      \begin{flagderiv}
+%        \assume{as-P}{P}{Assume:}
+%          \assume{as-Q}{Q}{Assume:}
+%            \step{re-P}{P}{Rei \ref{as-P}:}
+%         \conclude{imp1}{Q \implies P}
+%                        {$\implies$-intro on \ref{as-Q} and \ref{re-P}:}
+%        \conclude{imp2}{P \implies Q \implies P}
+%                        {$\implies$-intro on \ref{as-P} and \ref{imp1}:}
+%      \end{flagderiv}
+%    \end{Example}
+% 
+%    When the comments are inserted inline, a certain format is used, namely
+%    to enclose the comment with braces.  This is the default, but can be
+%    \DescribeMacro{\theinlcmnt}
+%    overridden by redefining the |\theinlcmnt| command.\index{override}
+%    \vspace{1em}
+% 
+%    \begin{Example}[gobble=7,frame=single,label=Changing inline comments format]
+%      \inlcmnts
+%      \renewcommand{\theinlcmnt}[1]{--#1--}
+%      \begin{flagderiv}
+%        \assume{ass-P}{P}{Assumption}
+%          \assume{ass-Q}{Q}{Assumption}
+%            \step{rei-P}{P}{Rei \ref{ass-P}}
+%      \end{flagderiv}
+%    \end{Example}
+% 
+%   \subsection{Namespaces for labels}
+%    In a document with a lot of auto-numbered derivations it is easy to lose
+%    overview of labels already used or it may be hard to keep thinking of
+%    new ones. To solve this a \flags\ environment can take a {\em namespace}
+%    as optional argument\index{namespacing}. This makes the lines referable 
+%    as normal within the same derivation but also globally when the namespace
+%    and a colon is added outside the derivation. For example a derivation for 
+%    Modus Tollens (MT):
+% 
+%    \begin{Example}[gobble=7,frame=single,label=Derivation label namespace]
+%      \begin{flagderiv}[mt]
+%        \step{s0}{P \implies Q}{}
+%        \assume{as-nQ}{\neg Q}{Assumption}
+%          \assume{as-P}{P}{Assumption}
+%            \step{s1}{Q}{$\implies$-elim on \ref{s0} and \ref{as-P}}
+%            \step{s2}{\bot}{$\bot$-intro on \ref{as-nQ} and \ref{s1}}
+%          \conclude{nP}{\neg P}{$\neg$-intro on \ref{as-P} and \ref{s2}} 
+%        \conclude{nQ-nP}{\neg Q \implies \neg P}
+%                        {$\implies$-intro on \ref{as-nQ} and \ref{nP}}
+%      \end{flagderiv}
+% 
+%      Note that step~\ref{mt:as-P} is not an intuitive step but necessary 
+%      to get $\neg P$ under the assumption $\neg Q$.
+%    \end{Example}
+% 
+%   \subsection{Other options}
+%    \DescribeMacro{\caption}\index{usage}
+%    \DescribeMacro{\tablehead}\DescribeMacro{\tablefirsthead}
+%    A \flags\ environment actually wraps a {\tt longtable}.  This means
+%    that at the start of an environment all {\tt longtable} options are
+%    available.  This means the use of |\caption|, and setting heads
+%    (|\tablehead| and |\tablefirsthead|) and feet (|\endfoot|
+%    \DescribeMacro{\endfoot}\DescribeMacro{\endlastfoot}
+%    and |\endlastfoot|) but also changing the lengths, etc.
+%
+%    \DescribeEnv{flagderiv*}
+%    Note that this does not hold for the slightly different |flagderiv*|
+%    environment, which acts exactly the same but is wrapped in a normal
+%    {\tt tabular} and thus can not be split across pages.
+%
+%    \begin{Example}[gobble=7,frame=single,label=Captioned]
+%      \inlcmnts
+%      \begin{flagderiv}[reflex]
+%        \caption{The reflexivity of $\equiv_n$} \\
+%        \introduce*{(1)}{x \in \All}{Assume:}
+%          \skipsteps*{\dots \\ \dots}{}
+%          \step*{(n - 1)}{x \equiv_n x}{}
+%        \conclude*{(n)}{\forall x \in \All: x \equiv_n x}
+%                       {$\forall$-intro on (1) and (n - 1):}
+%      \end{flagderiv}
+%    \end{Example}
+% 
+%    \DescribeMacro{\\}
+%    Additional it is possible to add custom newlines (|\\|) in all
+%    step formulas\footnote{This is not possible in introductions or
+%    assumptions, but they can often be split into multiple introductions or
+%    assumptions.} when the formula gets too long as demonstrated in the 
+%    above example.
+%
+% 
+%  \section{Examples\label{sec:ex}}
+%   The following are just a few real-life examples of flag-style proofs,
+%   where \flags\ provides an elegant means to include these proofs in
+%   \LaTeX-documents.
+% 
+%   \subsection{Examples from \flags}
+%    \subsection*{A derivation with auto-numbering and labels/references}
+%     \begin{flagderiv}
+%      \introduce{intro-xy}{x,y \in \mathbb{N}}{Introduction}
+%       \assume{assum:1}{x > 0}{Assumption}
+%        \assume{assum:2}{x < y}{Assumption}
+%         \step{y-pos}{y > 0}{Transitivity on \ref{assum:1} and \ref{assum:2}}
+%         \step{y3-pos}{y^3 > 0}{Arithmetic on \ref{y-pos}}
+%        \conclude{imp:1}{x < y \implies y^3 > 0}
+%                        {$\implies$-intro on \ref{assum:2} and \ref{y3-pos}}
+%       \conclude{imp:2}{x > 0 \implies x < y \implies y^3 > 0}
+%                       {$\implies$-intro on \ref{assum:1} and \ref{imp:1}}
+%      \conclude{}{\forall x, y \in \Nat: x > 0 \land x < y \implies y^3 > 0}
+%                 {$\forall$-intro on \ref{intro-xy} and \ref{imp:2}}
+%     \end{flagderiv}
+% 
+%    \subsection*{A derivation with manual numbering}
+%     \begin{flagderiv}
+%      \assume*{(m)}{\neg P}{}
+%       \skipsteps{1}{\dots}{}
+%       \step*{(n - 2)}{False}{}
+%      \conclude*{(n - 1)}{\neg\neg P}
+%                         {$\implies$-intro on (m) and (n - 2), and Negation}
+%      \step*{(n)}{P}{Double negation on (n - 1)}
+%     \end{flagderiv}
+% 
+% 
+%   \subsection{Predicate Calculus}
+%    \subsubsection*{Idempotence}
+%     \begin{flagderiv}[pc-idempotence]
+%      \assume{intro:PP}{P \land P}{}
+%       \step{and-elim:P}{P}{$\land$-elim on \ref{intro:PP}}
+%      \conclude{impl-intro:PP-P}{P \land P \implies P}
+%                                {$\implies$-intro on \ref{intro:PP}
+%                                 and \ref{and-elim:P}}
+%      \assume{intro:P}{P}{}
+%       \step{and-intro:P}{P \land P}{$\land$-intro on \ref{intro:P}
+%                                     and \ref{intro:P}}
+%      \conclude{impl-intro:P-PP}{P \implies P \land P}
+%                                {$\implies$-intro on \ref{intro:P}
+%                                 and \ref{and-intro:P}}
+%      \step{and-intro:result}{(P \land P \implies P) \land
+%                              (P \implies P \land P)}
+%                             {$\land$-intro on \ref{impl-intro:PP-P}
+%                              and \ref{impl-intro:P-PP}}
+%      \step{idempotence}{P \land P \equiv P}
+%                        {$\equiv$-intro on \ref{and-intro:result}}
+%     \end{flagderiv}
+% 
+%    \subsubsection*{De Morgan}
+%     \begin{flagderiv}[pc-demorgan]
+%      \assume{intro:NPQ}{\lnot (P \land Q)}{}
+%       \assume{intro:NNP}{\lnot\lnot P}{}
+%        \assume{intro:Q}{Q}{}
+%         \step{notnot-elim:P}{P}{$\lnot\lnot$-elim on \ref{intro:NNP}}
+%        \step{and-intro:PQ}{P \land Q}{$\land$-intro on \ref{intro:Q}
+%                                       and \ref{notnot-elim:P}}
+%         \step{false-intro:2}{\false}
+%                             {$\false$-intro on \ref{and-intro:PQ}
+%                              and \ref{intro:NPQ}}
+%        \conclude{not-intro:Q}{\lnot Q}{$\lnot$-intro on \ref{intro:Q}
+%                                        and \ref{false-intro:2}}
+%       \conclude{impl-intro:NNP-NQ}{\lnot\lnot P \implies \lnot Q}
+%                                   {$\implies$-intro on \ref{intro:NNP}
+%                                    and \ref{not-intro:Q}}
+%       \step{or-intro:NP-NQ}{\lnot P \lor \lnot Q}
+%                            {$\lor$-intro on \ref{impl-intro:NNP-NQ}}
+%      \conclude{impl-intro:NPQ-NPNQ}{\lnot (P \land Q) \implies
+%                                     \lnot P \lor \lnot Q}
+%                                    {$\implies$-intro on \ref{intro:NPQ}
+%                                     and \ref{or-intro:NP-NQ}}
+%      \assume{intro:NPNQ}{\lnot P \land \lnot Q}{}
+%       \assume{intro:PQ}{P \lor Q}{}
+%        \step{or-elim:NP-Q}{\lnot P \implies Q}
+%                           {$\lor$-elim on \ref{intro:PQ}}
+%        \step{and-elim:NP}{\lnot P}{$\land$-elim on \ref{intro:NPNQ}}
+%        \step{impl-elim:Q}{Q}{$\implies$-elim on \ref{or-elim:NP-Q}
+%                              and \ref{and-elim:NP}}
+%        \step{and-elim:NQ}{\lnot Q}{$\land$-elim on \ref{intro:NPNQ}}
+%        \step{false-intro:1}{\false}{$\false$-intro on \ref{impl-elim:Q}
+%                                     and \ref{and-elim:NQ}}
+%       \conclude{impl-intro:PQ}{P \lor Q \implies \false}
+%                               {$\implies$-intro on \ref{intro:PQ}
+%                                and \ref{false-intro:1}}
+%       \step{not-intro:PQ}{\lnot (P \lor Q)}
+%                          {$\lnot$-intro on \ref{impl-intro:PQ}}
+%      \conclude{impl-intro:NPNQ-NPQ}{\lnot P \land \lnot Q \implies
+%                                     \lnot (P \lor Q)}
+%                                    {$\implies$-intro on \ref{intro:NPNQ}
+%                                     and \ref{not-intro:PQ}}
+%      \step{and-intro:result}{(\lnot (P \land Q) \implies
+%                               \lnot P \lor \lnot Q)
+%                              \land\\
+%                              (\lnot P \land \lnot Q \implies
+%                               \lnot (P \lor Q))}
+%                             {$\land$-intro on \ref{impl-intro:NPQ-NPNQ}
+%                              and \ref{impl-intro:NPNQ-NPQ}}
+%      \step{demorgan}{\lnot (P \land Q) \equiv \lnot P \lor \lnot Q}
+%                     {$\equiv$-intro on \ref{and-intro:result}}
+%     \end{flagderiv}
+% 
+%    \subsubsection*{Transitivity}
+%     \begin{flagderiv}[pc-transitivity]
+%      \introduce{intro:PQR}{P, Q, R}{}
+%       \assume{intro:PQQR}{(P \implies Q) \land (Q \implies R)}{}
+%        \assume{intro:P}{P}{}
+%         \step{and-elim:PQ}{P \implies Q}
+%                           {$\land$-elim on \ref{intro:PQQR}}
+%         \step{impl-elim:Q}{Q}{$\implies$-elim on \ref{and-elim:PQ}
+%                               and \ref{intro:P}}
+%         \step{and-elim:QR}{Q \implies R}
+%                           {$\land$-elim on \ref{intro:PQQR}}
+%         \step{impl-elim:R}{R}{$\implies$-elim on \ref{and-elim:QR}
+%                               and \ref{impl-elim:Q}}
+%        \conclude{impl-intro:PR}{P \implies R}
+%                                {$\implies$-intro on \ref{intro:P}
+%                                 and \ref{impl-elim:R}}
+%       \conclude{impl-intro:PQQR-PR}{(P \implies Q) \land (Q \implies R)
+%                                     \implies (P \implies R)}
+%                                    {$\implies$-intro on \ref{intro:PQQR}
+%                                     and \ref{impl-intro:PR}}
+%      \conclude{transitivity}{(\forall P, Q, R::
+%                               (P \implies Q) \land (Q \implies R)
+%                               \implies (P \implies R)
+%                              )}
+%                             {$\forall$-intro on \ref{intro:PQR}
+%                              and \ref{impl-intro:PQQR-PR}}
+%     \end{flagderiv}
+% 
+%   \subsection{Rewrite Systems}
+%    \subsubsection*{Mixed confluent $\biimplies$ Church-Rosser}
+%     {
+%      \renewcommand{\introsymb}{\text{Let}}
+%      \begin{flagderiv}
+%       \assume*{1}{\CRtext}{hyp}
+%        \introduce*{2}{a, b, c\in A, \text{such that}~a\OHA b\land a\THA c}{}
+%         \step*{3}{a\OHA b\land a\THA c}{rei (2)}
+%         \step*{4}{a\THA b\land a\THA c}{$\forall$-elimination on lemma~\ref{transclosure} and (3)}
+%         \step*{5}{(\exists d\in A:: b\THA d\land c\THA d)}{$\forall$-elimination on (1) and (4)}
+%        \conclude*{6}{\MCtext}{$\forall$-introduction on (2) and (5)}
+%       \conclude*{7}{\CRtext\implies\MCtext}{$\implies$-introduction on (1) and (6)}
+%       \assume*{8}{\MCtext}{}
+%        \assume*{9}{\text{Induction on the length of}~a\THA b}{}
+%         \skipsteps*{\IHbase}{}
+%         \introduce*{11}{a, b, c\in A, \text{such that}~a\NHA{0} b\land a\THA c}{}
+%          \step*{12}{a=b}{def $\NHA{0}$, (11)}
+%          \step*{13}{a\THA c}{$\land$-elimination on (11)}
+%          \step*{14}{b\THA c}{(12) applied on (13)}
+%          \step*{15}{c\THA c \land b\THA c}{}
+%          \step*{16}{(\exists d\in A:: b\THA d\land c\THA d)}{}
+%         \renewcommand{\thesteplabel}[1]{#1}
+%         \conclude*{}{\IHhyp}{}
+%         \step*{18}{\ensuremath{(\forall a, b, c\in A: a\NHA{n} b\land a\THA c:\\ \quad
+%                                 (\exists d\in A:: b\THA d\land c\THA d))}}{}
+%         \skipsteps*{\IHstep}{}
+%         \introduce*{20}{a, b, c\in A, \text{such that}~a\NHA{n+1} b\land a\THA c}{}
+%          \step*{21}{a\NHA{n+1} b}{$\land$-elimination on (20)}
+%          \step*{22}{a\NHA{n} b'\OHA b}{}
+%          \step*{23}{a\THA c}{$\land$-elimination on (20)}
+%          \step*{24}{a\NHA{n} b' \land a\THA c}{$\land$-introduction on (22) and (23)}
+%          \step*{25}{(\exists d'\in A:: b'\THA d'\land c\THA d')}{$\forall$-elimination on (18) and  (24)}
+%          \step*{26}{d', \text{such that}~b'\THA d'\land c\THA d'}{$\exists$-elimination on (25)}
+%          \step*{27}{b'\OHA b \land b'\THA d'}{}
+%          \step*{28}{(\exists d\in A:: b\THA d\land d'\THA d)}{$\forall$-elimination on (8) and (27)}
+%          \step*{29}{d, \text{such that}~b\THA d\land d'\THA d}{$\exists$-elimination on (28)}
+%          \step*{30}{a\NHA{n} b'\OHA b\THA d \land a\THA c\THA d'\THA d}{}
+%          \step*{31}{b\THA d \land c\THA d}{}
+%          \step*{32}{(\exists d\in A:: b\THA d\land c\THA d)}{}
+%        \conclude*[2]{33}{\CRtext}{}
+%       \conclude*{34}{\MCtext\implies\CRtext}{$\implies$-introduction on (8) and (33)}
+%       \step*{35}{\MCtext\biimplies\CRtext}{$\biimplies$-introduction on (7) and (34)}
+%      \end{flagderiv}
+%     }
+% 
+%     \begin{lemma}
+%      \label{transclosure}
+%      \mbox{\ensuremath{(\forall a, b\in A: a\OHA b: a\THA b)}}
+%     \end{lemma}
+%
+% \StopEventually{}
+%
+% \newpage
+% \section{Implementation}
+%
+%  First some initial code is needed for processing of the options.
+%  Note that {\tt ifthen} is used throughout the package.
+%    \begin{macrocode}
+\RequirePackage{ifthen}
+\newboolean{@inlcmnts}
+%    \end{macrocode}
+% 
+%  Processing of the option ({\tt inlcmnts}) for enabling inline comments.
+%    \begin{macrocode}
+\DeclareOption{inlcmnts}{\setboolean{@inlcmnts}{true}}
+\ProcessOptions
+%    \end{macrocode}
+%
+%  Loading of the required packages.
+%  Note that \flags\ needs to require a fix/override for the array package, 
+%  until the fixed version is available in most distributions.
+%    \begin{macrocode}
+\RequirePackage{array}
+\RequirePackage{longtable}
+\long\@namedef{NC@rewrite@*}#1#2{%
+   \count@#1\relax
+   \loop
+   \ifnum\count@>\z@
+   \advance\count@\m@ne
+   \@temptokena\expandafter{\the\@temptokena#2}%
+   \repeat
+   \NC@find}
+%    \end{macrocode}
+%
+% \subsection{Generic settings, counters and commands}
+%
+%  \begin{macro}{fd@flagcount}
+%  \begin{macro}{fd@stepcount}
+%   The counters keeping the number of opened/nested flags and the number of
+%   derivation steps.
+%    \begin{macrocode}
+\newcounter{fd@flagcount}
+\newcounter{fd@stepcount}
+%    \end{macrocode}
+%  \end{macro}
+%  \end{macro}
+%  
+%  \begin{macro}{\derivskip}
+%   The default space ({\tt 8pt}) between lines in a derivation.  This is 
+%   overridable to define  a different default length.
+%    \begin{macrocode}
+\newlength{\derivskip}
+\setlength{\derivskip}{8pt}
+%    \end{macrocode}
+%  \end{macro}
+%
+%  \begin{macro}{\introsymb}
+%   The symbol used as variable introduction prefix.  Overridable with
+%   |\renewcommand| to insert a different symbol, defaults to: 
+%   |\textbf{var}|.
+%
+%   Ex. |\renewcommand{\introsymb}{\textbf{Let}}|
+%    \begin{macrocode}
+\newcommand{\introsymb}{\textbf{var}}
+%    \end{macrocode}
+%  \end{macro}
+%
+%  \begin{macro}{\thestepcount}
+%   This is the command used to generate a step number label (used by 
+%   auto-numbering). |\thestepcount| can be overridden to display labels 
+%   differently, defaults to: ({\it number}). This exposes the internal
+%   |\thefd@stepcount| command.
+%
+%   Ex. |\renewcommand{\thestepcount}{[\arabic{stepcount}]}|
+%    \begin{macrocode}
+\newcommand{\thestepcount}{(\arabic{fd@stepcount})}
+\renewcommand{\thefd@stepcount}{\thestepcount}
+%    \end{macrocode}
+%  \end{macro}
+%
+%  \begin{macro}{\thesteplabel}
+%   Command used to generate a customized step label (used by manual numbering).
+%   |\thesteplabel| can be overridden to display manual numbers differently,
+%   this command has one argument: \marg{label}.
+%   The command does nothing by default (i.e\@. just returns the argument).
+%
+%   Ex. |\renewcommand{\thesteplabel}[1]{[##1]}|
+%    \begin{macrocode}
+\newcommand{\thesteplabel}[1]{#1}
+%    \end{macrocode}
+%  \end{macro}
+%
+%  \begin{macro}{\theinlcmnt}
+%   The command used to format inline comments (if enabled).  |\theinlcmnt| 
+%   can be overridden to display it differently and has one argument: 
+%   \marg{comment}. Defaults to: \{ {\em comment text} \}.
+%
+%   Ex. |\renewcommand{\theinlcmnt}[1]{--#1--}|
+%    \begin{macrocode}
+\newcommand{\theinlcmnt}[1]{\{ #1 \}}
+%    \end{macrocode}
+%  \end{macro}
+%
+%  \begin{macro}{\inlcmnts}
+%   Command to switch inline comments explicitly on (and by that, overriding
+%   and forgetting the default determined by the absence or presence of the
+%   {\tt inlcmnts} package option).
+%
+%    \begin{macrocode}
+\newcommand{\inlcmnts}{\setboolean{@inlcmnts}{true}}
+%    \end{macrocode}
+%  \end{macro}
+%
+%  \begin{macro}{\noinlcmnts}
+%   Command to switch inline comments explicitly off (and by that, overriding
+%   and forgetting the default determined by the absence or presence of the
+%   {\tt inlcmnts} package option).
+%
+%    \begin{macrocode}
+\newcommand{\noinlcmnts}{\setboolean{@inlcmnts}{false}}
+%    \end{macrocode}
+%  \end{macro}
+%
+% \subsection{The derivation environment}
+%
+% The following three sections describe the internal commands and constructs
+% of the {\tt flagderiv} environment, after which the last section will
+% explain how the environment works and how it is put together using the
+% internal constructs.
+%
+% Note that for almost all commands there exists two versions, one used
+% for manual numbered derivations and one for automatic numbered/labelled
+% derivations (both forms can be mixed within the environment).
+%
+% \subsubsection{Labels}
+%
+% Derivation lines are labelled and can be referred to.  This can be done
+% with automatically numbered lines where the first argument is a normal
+% \LaTeX\ label.  However, to avoid clashing, the labels can be automatically
+% prefixed with a namespace. The following two commands handle this prefixing.
+%
+%  \begin{macro}{\@labelprefix}
+%   Command that specifies the label namespace prefix.
+%
+%    \begin{macrocode}
+\newcommand{\@labelprefix}{\relax}
+%    \end{macrocode}
+%   \end{macro}
+%  \begin{macro}{\@derlabel}
+%   Internal command to define a label using the prefix (if a label
+%   is defined, otherwise do nothing).
+%
+%    \begin{macrocode}
+\newcommand{\@derlabel}[1]{%
+  \ifthenelse{\equal{#1}{}}{}{\label{\@labelprefix#1}}%
+}
+%    \end{macrocode}
+%  \end{macro}
+%
+% \subsubsection{Steps}
+% 
+% A line of a derivation can be one of five types:
+% \begin{enumerate}
+%  \item A simple and bare line, only internally accessible,
+%  \item a comment line,
+%  \item a derivation step (both automatically and manual numbered),
+%  \item a line to indicate skipping of steps,
+%  \item a flag (handled in the next section).
+% \end{enumerate}
+%
+% This section deals with the first four types.
+%
+%  \begin{macro}{\@derline}
+%   A simple derivation line that uses {\tt fd@flagcount} to remember
+%   the number of open flags. This command is used as:
+%   |\@derline|\marg{label}\marg{formula}\marg{comment}, with:
+%   \begin{description}
+%    \item[\marg{label}] a label which can be left empty, to refer back to in 
+%     comments of other derivation lines,
+%    \item[\marg{formula}] the formula, and
+%    \item[\marg{comment}] a comment.
+%   \end{description}
+%
+%    \begin{macrocode}
+\newcommand{\@derline}[3]{%
+ \mbox{#1} &
+ \setlength{\extrarowheight}{\derivskip}%
+%    \end{macrocode}
+%   If the flag counter is still zero\dots
+%    \begin{macrocode}
+ \ifthenelse{\value{fd@flagcount}=0}%
+%    \end{macrocode}
+%   then this line is outside any flag,
+%    \begin{macrocode}
+ {\begin{array}[t]{@{}l}}%
+%    \end{macrocode}
+%   otherwise this is inside one or more flag contexts and the amount of
+%   open flagpoles equal to the number of open contexts should be inserted.
+%
+%    \begin{macrocode}
+ {\begin{array}[t]{*{\value{fd@flagcount}}{|@{\hspace{2\arraycolsep}}}l}}
+  \ensuremath{#2}
+ \end{array} &
+ \mbox{#3} \\
+}
+%    \end{macrocode}
+%  \end{macro}
+%
+%  \begin{macro}{\@CMNTderline}
+%   Command to fold the comment on a separate line before the
+%   actual derivation line if the {\tt inlcmnts} option is set for this
+%   package, see also |\@derline| for the argument handling.
+%
+%    \begin{macrocode}
+\newcommand{\@CMNTderline}[3]{%
+ \ifthenelse{\boolean{@inlcmnts}}{%
+%    \end{macrocode}
+%   If the inline comments option is enabled, fold the comment before the 
+%   actual line.
+%    \begin{macrocode}
+  \ifthenelse{\equal{#3}{}}{}{% 
+%    \end{macrocode}
+%   There is comment, insert it inline.
+%    \begin{macrocode}
+   \@derline{}{\mbox{\theinlcmnt{#3}}}{}%
+  }
+  \@derline{#1}{#2}{}%
+ }{%
+%    \end{macrocode}
+%   If inline comments are not enabled, pass everything to |\@derline| directly.
+%    \begin{macrocode}
+  \@derline{#1}{#2}{#3}%
+ }%
+}
+%    \end{macrocode}
+%  \end{macro}
+%
+%  \begin{macro}{\@MANstep}
+%  \begin{macro}{\@AUTOstep}
+%   Command for the manual ({\tt MAN}) and automatically ({\tt AUTO})
+%   numbered version of a derivation step.  See also |\@derline|.
+%
+%    \begin{macrocode}
+\newcommand{\@MANstep}[3]{\@CMNTderline{\thesteplabel{#1}}{#2}{#3}}
+%    \end{macrocode}
+%
+%    \begin{macrocode}
+\newcommand{\@AUTOstep}[3]{%
+ \refstepcounter{fd@stepcount}%
+ \@derlabel{#1}\@CMNTderline{\thestepcount}{#2}{#3}%
+}
+%    \end{macrocode}
+%  \end{macro}
+%  \end{macro}
+%
+%  \begin{macro}{\@MANskipsteps}
+%  \begin{macro}{\@AUTOskipsteps}
+%   Command for the manual ({\tt MAN}) and automatically ({\tt AUTO})
+%   numbered version of skipping derivation steps.  See also |\@derline|.
+%
+%    \begin{macrocode}
+\newcommand{\@MANskipsteps}[2]{\@CMNTderline{}{#1}{#2}}
+%    \end{macrocode}
+%
+%    \begin{macrocode}
+\newcommand{\@AUTOskipsteps}[3]{%
+ \addtocounter{fd@stepcount}{#1}%
+ \@CMNTderline{}{#2}{#3}%
+}
+%    \end{macrocode}
+%  \end{macro}
+%  \end{macro}
+%
+% \subsubsection{Flags}
+%
+% Flags are actually simple derivation lines with two extras: the formula
+% is put into a flag box and the flag counter {\tt fd@flagcount} is incremented
+% when one is opened.  Next to flag commands there are also commands to
+% to close (and by that decrementing the counter) flags.
+%
+% There exist three types of flags:
+% \begin{enumerate}
+%  \item the simple and bare flag,
+%  \item the assumption flag (both manual and automatically numbered),
+%  \item the variable introduction flag (also manual and automatically numbered).
+% \end{enumerate}
+%
+%  \begin{macro}{\@flagbox}
+%   Creates a flag for (a box around) the given text/formula, takes
+%   \marg{formula} as an argument.
+%    \begin{macrocode}
+\newcommand{\@flagbox}[1]{%
+ \setlength{\fboxsep}{0.75ex}%
+ \fbox{#1}%
+}
+%    \end{macrocode}
+%  \end{macro}
+%
+%  \begin{macro}{\@startflag}
+%   Starts a flag context by opening a flag and incrementing the counter.
+%   The command is used as:
+%   |\@startflag|\marg{label}\marg{formula}\marg{comment},
+%   see also |\@derline| for the meaning of these arguments.
+%
+%    \begin{macrocode}
+\newcommand{\@startflag}[3]{%
+ \@CMNTderline{#1}{\@flagbox{\ensuremath{#2}}}{#3}%
+ \addtocounter{fd@flagcount}{1}%
+}
+%    \end{macrocode}
+%  \end{macro}
+%
+%  \begin{macro}{\@endflag}
+%   Ends a flag by closing it and decrementing the counter.  Takes the
+%   number of flags to close \marg{number} as an argument.
+%
+%    \begin{macrocode}
+\newcommand{\@endflag}[1]{\addtocounter{fd@flagcount}{-#1}}
+%    \end{macrocode}
+%  \end{macro}
+%
+%  \begin{macro}{\@flagclose}
+%   Wrapper command for closing a number of flags simultaneously taking \oarg{number}
+%   as an optional argument, defaulting to 1. See also |\@endflag|.
+%
+%    \begin{macrocode}
+\newcommand{\@flagclose}[1][1]{\@endflag{#1}}
+%    \end{macrocode}
+%  \end{macro}
+%
+%  \begin{macro}{\@MANassume}
+%  \begin{macro}{\@AUTOassume}
+%   Command for the manual ({\tt MAN}) and automatic ({\tt AUTO}) 
+%   numbered version of an assumption flag, see also |\@startflag|.
+%
+%    \begin{macrocode}
+\newcommand{\@MANassume}[3]{\@startflag{\thesteplabel{#1}}{#2}{#3}}
+%    \end{macrocode}
+%
+%    \begin{macrocode}
+\newcommand{\@AUTOassume}[3]{
+ \refstepcounter{fd@stepcount}%
+ \@derlabel{#1}\@startflag{\thestepcount}{#2}{#3}%
+}
+%    \end{macrocode}
+%  \end{macro}
+%  \end{macro}
+%
+%  \begin{macro}{\@MANintroduction}
+%  \begin{macro}{\@AUTOintroduction}
+%   Command for the manual ({\tt MAN}) and automatically ({\tt AUTO}) 
+%   numbered version of an introduction flag, see also |\@startflag|.
+%
+%    \begin{macrocode}
+\newcommand{\@MANintroduction}[3]{%
+  \@startflag{\thesteplabel{#1}}{\introsymb~#2}{#3}%
+}
+%    \end{macrocode}
+%
+%    \begin{macrocode}
+\newcommand{\@AUTOintroduction}[3]{
+  \refstepcounter{fd@stepcount}%
+  \@derlabel{#1}\@startflag{\thestepcount}{\introsymb~#2}{#3}%
+}
+%    \end{macrocode}
+%  \end{macro}
+%  \end{macro}
+%
+%  \begin{macro}{\@MANconclude}
+%  \begin{macro}{\@AUTOconclude}
+%   Command to conclude from one or more open flags in the manual ({\tt MAN}) 
+%   and automatically ({\tt AUTO}) numbered version, see also |\@endflag|.  
+%   The command is used as: 
+%   |\@MANconclude|\oarg{number}\marg{label}\marg{formula}\marg{comment},
+%   where the \oarg{number} indicates the number of flags to close,
+%   defaulting to 1.
+%
+%    \begin{macrocode}
+\newcommand{\@MANconclude}[4][1]{\@endflag{#1}\step*{#2}{#3}{#4}}
+%    \end{macrocode}
+%
+%    \begin{macrocode}
+\newcommand{\@AUTOconclude}[4][1]{\@endflag{#1}\step{#2}{#3}{#4}}
+%    \end{macrocode}
+%  \end{macro}
+%  \end{macro}
+%
+% \subsubsection{The environment itself}
+%
+%  \begin{environment}{flagderiv}
+%   This section explains the main environment for flag style
+%   derivations/proofs:  {\tt flagderiv}.  The command has an optional
+%   argument \oarg{prefix}, used as label prefix so that labels can be
+%   ``scoped'' with a namespace local to the derivation but still 
+%   accessible from the outside.
+% 
+%   Examples:\\
+%   |\begin{flagderiv} ... \end{flagderiv}|\\
+%   |\begin{flagderiv}[abs] ... \end{flagderiv}|
+% 
+%    \begin{macrocode}
+\newenvironment{flagderiv}[1][]{%
+%    \end{macrocode}
+%
+%  First, set the optional label prefix (if given) and reset the counters.
+%
+%    \begin{macrocode}
+ \ifthenelse{\equal{#1}{}}{%
+  \renewcommand{\@labelprefix}{}%
+ }{%
+  \renewcommand{\@labelprefix}{#1:}%
+ }%
+ \setcounter{fd@flagcount}{0}%
+ \setcounter{fd@stepcount}{0}%
+%    \end{macrocode}
+%
+%  Note: {\em All} of the following five commands have a star version which
+%  allows manual numbering, instead of having auto-numbering, \LaTeX\ labels 
+%  and references.
+%
+%  \begin{macro}{\assume}
+%  \begin{macro}{\assume*}
+%   Opens an assumption flag; command usage:\\[1em]
+%   |\assume|\marg{label}\marg{formula}\marg{comment}\\
+%   |\assume*|\marg{custom-number}\marg{formula}\marg{comment}
+%
+%   Examples: \\
+%   |\assume{assum:1}{x > 0}{Assumption}|\\
+%   |\assume*{l}{\neg P}{}|
+%
+%    \begin{macrocode}
+ \newcommand{\assume}{\@ifstar{\@MANassume}{\@AUTOassume}}
+%    \end{macrocode}
+%  \end{macro}
+%  \end{macro}
+%
+%  \begin{macro}{\introduce}
+%  \begin{macro}{\introduce*}
+%   Opens an introduction flag. Command usage: \\[1em]
+%   |\introduce|\marg{label}\marg{formula}\marg{comment} \\
+%   |\introduce*|\marg{custom-number}\marg{formula}\marg{comment}
+%
+%   Examples:\\
+%   |\introduce{intro-x}{x \in \mathbb{N}}{Introduction}| \\
+%   |\introduce*{l - 1}{P \in s_P}{}|
+%
+%    \begin{macrocode}
+ \newcommand{\introduce}{\@ifstar{\@MANintroduction}{\@AUTOintroduction}}
+%    \end{macrocode}
+%  \end{macro}
+%  \end{macro}
+%
+%  \begin{macro}{\conclude}
+%  \begin{macro}{\conclude*}
+%   Performs a conclusion/multiple conclusion from one or more
+%   introductions and/or assumptions. The command usage:\\[1em]
+%   |\conclude|\oarg{number}\marg{label}\marg{formula}\marg{comment}\\
+%   |\conclude*|\oarg{number}\marg{custon-number}\marg{formula}\marg{comment}
+%
+%   The optional argument \oarg{number} indicates how much flags should be 
+%   closed with this conclusion, this defaults to 1.
+%
+%   Examples;\\
+%   |\conclude[2]{concl:2}{x > 0 \implies ...}{$\implies$-intro on ...}|\\
+%   |\conclude*{n - 1}{\neg\neg P}{$\implies$-intro on (l) ...}|
+%
+%    \begin{macrocode}
+ \newcommand{\conclude}{\@ifstar{\@MANconclude}{\@AUTOconclude}}
+%    \end{macrocode}
+%   \end{macro}
+%   \end{macro}
+%
+%   \begin{macro}{\step}
+%   \begin{macro}{\step*}
+%    Performs a derivation step, command usage:\\[1em]
+%    |\step|\marg{label}\marg{formula}\marg{comment}\\
+%    |\step*|\marg{custom-number}\marg{formula}\marg{comment} 
+%
+%    Examples:\\
+%    |\step{x-elim}{x > 0}{$\forall$-elem on \ref{assum:1}}|\\
+%    |\step*{n - 1}{x > 0}{$\forall$-elem on (n - 3)}|
+%
+%    Note: |\\| (line breaks) may be inserted for splitting
+%    large formulas.
+%
+%    \begin{macrocode}
+ \newcommand{\step}{\@ifstar{\@MANstep}{\@AUTOstep}}
+%    \end{macrocode}
+%  \end{macro}
+%  \end{macro}
+%
+%  \begin{macro}{\skipsteps}
+%  \begin{macro}{\skipsteps*}
+%    Skips a number of steps (for usage in examples), usage:\\[1em]
+%    |\skipsteps|\marg{number}\marg{formula}\marg{comments}\\
+%    |\skipsteps*|\marg{formula}\marg{comments}.
+%
+%    Examples:\\
+%    |\skipsteps{3}{\vdots}{Etcetera, etcetera}|\\
+%    |\skipsteps*{\vdots}{Etcetera, etcetera}|
+%
+%    \begin{macrocode}
+ \newcommand{\skipsteps}{\@ifstar{\@MANskipsteps}{\@AUTOskipsteps}}
+%    \end{macrocode}
+%  \end{macro}
+%  \end{macro}
+%
+%  \begin{macro}{\done}
+%   Closes a number of flags because contexts have been opened and
+%   should be closed without conclusions.  Command usage: \\[1em]
+%   |\done|\oarg{number}
+%
+%   This command takes a number of introductions/assumptions, \oarg{number},
+%   to close as an optional argument, which defaults to 1.
+%
+%   Examples:\\
+%   |\done|\\
+%   |\done[3]|
+%
+%    \begin{macrocode}
+ \newcommand{\done}{\@flagclose}
+%    \end{macrocode}
+%  \end{macro}
+%
+%  Silently override |\ref| to work with the defined namespace.
+%    \begin{macrocode}
+ \let\origref\ref%
+ \renewcommand{\ref}[1]{\origref{\@labelprefix##1}}%
+%    \end{macrocode}
+%
+% The actual flagderiv environment is just a longtable (called
+% ``derivation'').
+%
+%    \begin{macrocode}
+ \renewcommand{\tablename}{Derivation}%
+ \begin{longtable}[l]{rll}
+}{%
+ \end{longtable}
+}
+%    \end{macrocode}
+%  \end{environment}
+%
+%  \begin{environment}{flagderiv*}
+%   The |flagderiv*| environment is almost the same as |flagderiv|
+%   with the only difference that the resulting derivation will and
+%   can not be split across pages.
+%
+%   Example:\\
+%   |\begin{flagderiv*} ... \end{flagderiv*}|\\
+% 
+%    \begin{macrocode}
+\newenvironment{flagderiv*}[1][]{%
+ \ifthenelse{\equal{#1}{}}{%
+  \renewcommand{\@labelprefix}{}%
+ }{%
+  \renewcommand{\@labelprefix}{#1:}%
+ }%
+ \setcounter{fd@flagcount}{0}%
+ \setcounter{fd@stepcount}{0}%
+ \newcommand{\assume}{\@ifstar{\@MANassume}{\@AUTOassume}}
+ \newcommand{\introduce}{\@ifstar{\@MANintroduction}{\@AUTOintroduction}}
+ \newcommand{\conclude}{\@ifstar{\@MANconclude}{\@AUTOconclude}}
+ \newcommand{\step}{\@ifstar{\@MANstep}{\@AUTOstep}}
+ \newcommand{\skipsteps}{\@ifstar{\@MANskipsteps}{\@AUTOskipsteps}}
+ \newcommand{\done}{\@flagclose}
+ \let\origref\ref%
+ \renewcommand{\ref}[1]{\origref{\@labelprefix##1}}%
+ \renewcommand{\tablename}{Derivation}
+ \begin{tabular}{rll}
+}{%
+ \end{tabular}
+}
+%    \end{macrocode}
+%  \end{environment}
+%
+% \PrintIndex
+% \PrintChanges
+%
+% \Finale
+\endinput
diff --git a/Master/texmf-dist/source/latex/flagderiv/flagderiv.ins b/Master/texmf-dist/source/latex/flagderiv/flagderiv.ins
new file mode 100644
index 00000000000..2dfc581c97d
--- /dev/null
+++ b/Master/texmf-dist/source/latex/flagderiv/flagderiv.ins
@@ -0,0 +1,63 @@
+%%
+%% Copyright (C) 2005 by Paul van Tilburg <paul@luon.net>
+%%
+%% This package is free software; you can redistribute it and/or modify
+%% it under the terms of the GNU General Public License as published by
+%% the Free Software Foundation; either version 2 of the License, or
+%% (at your option) any later version.
+%%
+%% This package is distributed in the hope that it will be useful,
+%% but WITHOUT ANY WARRANTY; without even the implied warranty of
+%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+%% GNU General Public License for more details.
+%%
+%% You should have received a copy of the GNU General Public License
+%% along with this package; if not, write to the Free Software
+%% Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+
+\input docstrip.tex
+\keepsilent
+
+\usedir{tex/latex/flagderiv}
+
+\preamble
+
+This is a generated file.
+
+Copyright (C) 2005 by Paul van Tilburg <paul@luon.net>
+
+This package is free software; you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation; either version 2 of the License, or
+(at your option) any later version.
+
+This package is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this package; if not, write to the Free Software
+Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+
+\endpreamble
+
+\generate{\file{flagderiv.sty}{\from{flagderiv.dtx}{flagderiv}}}
+%\generate{\file{farray.sty}{\from{farray.dtx}{farry}}}
+
+\obeyspaces
+\Msg{*************************************************************}
+\Msg{*                                                           *}
+\Msg{* To finish the installation you have to move the following *}
+\Msg{* file into a directory searched by TeX:                    *}
+\Msg{*                                                           *}
+\Msg{*     flagderiv.sty                                         *}
+\Msg{*                                                           *}
+\Msg{* To produce the documentation run the file flagderiv.dtx   *}
+\Msg{* through LaTeX.                                            *}
+\Msg{*                                                           *}
+\Msg{* Happy TeXing!                                             *}
+\Msg{*                                                           *}
+\Msg{*************************************************************}
+
+\endbatchfile