finish deleting proofs

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

7 files changed, 0 insertions, 2425 deletions

diff --git a/Master/texmf-dist/source/latex/proofs/taylor/QED-.sty b/Master/texmf-dist/source/latex/proofs/taylor/QED-.sty
deleted file mode 100644
index 788479059a9..00000000000
--- a/Master/texmf-dist/source/latex/proofs/taylor/QED-.sty
+++ /dev/null
@@ -1,580 +0,0 @@
-\message{<Paul Taylor's right-justified end-of-proof mark, 2 June 1993>}
-%%========================================================================
-%************************************************************************%
-%*									*%
-%*	Maybe you already have a \qed macro to put a little square	*%
-%*      on the right hand side at the end of a mathematical proof?	*%
-%*									*%
-%*			IT'S PROBABLY MINE!				*%
-%*									*%
-%*	     Please compare yours with \parag@pushright below.		*%
-%*									*%
-%*	This new file is compatible, it fixes the bugs, has extra	*%
-%*	features, and is maintained and portable.  Please use it!	*%
-%*									*%
-%************************************************************************%
-%========================================================================%
-
-% COPYRIGHT (C) 1993 Paul Taylor, Imperial College, London SW7 2BZ, UK
-% You may use this file for any purpose. You may copy it on condition that
-% you do so in exactly the form in which it was supplied, make no charge
-% for the copy and impose the same conditions on the recipient.
-% This software is supplied ``as is'' without warranty, express or implied,
-% including but not limited to merchantability and fitness for any particular
-% purpose. No liability is accepted by the author, Imperial College or any
-% third party for any direct or consequential damages, however caused.
-% In all cases you must keep several backup versions of your files in a place
-% to which your machine cannot write, and you must check documents visually
-% before submitting the final version to a publisher or expensive printer.
-
-% WARNING: If you use this with Frank Mittlebach's "theorem.sty" you
-% MUST load theorem first, then QED, then do the \newtheorem commands.
-% "theorem.sty" provides a number of typographical styles and is
-% available by anonymous ftp from ftp.uni-stuttgart.de (129.69.1.12)
-% in the directory         /pub/soft/tex/macros/latex/styles/base/theorem
-% also Aston: ftp.tex.ac.uk:/pub/archive/macros/latex/styles/base/theorem
-
-%	Authoritative version:	/tex/contrib/Taylor/tex/QED.sty
-%	by anonymous FTP from:	theory.doc.ic.ac.uk (146.169.2.27)
-%	author/maintained by:	Dr Paul Taylor <pt@doc.ic.ac.uk>
-
-% WARNING: This file replaces some of the functions of "Paul.sty"
-% and MUST NOT be used with it as serious conflicts will arise.
-% A new version is available as /tex/contrib/Taylor/Paul.sty as above.
-
-%=========================================================================
-
-%	USER INTERFACE AND EXAMPLES (see also OPTIONS below)
-
-%	\begin{Proof} ... \end{Proof}
-%	or    \Proof  ... \endProof
-%	or    \Proof  ... \endproof
-%	or    \Proof  ... \qed		also \QED and \QEI
-
-% WARNING: \qed which doesn't follow \Proof will not print the square.
-
-% Each properly nested Proof/endProof pair gets a single
-% \qedsymbol at the end, on the far right hand side.
-% Unfortunately, this may still be in the wrong place
-% if the proof ends with a display or itemisation.
-% To solve this, \qed may be put *inside* the last substantive
-% environment; the \qedsymbol will be put at that point
-% (the visual end) and suppressed at the logical end of proof.
-
-% Examples:
-%	\begin{Proof}			\begin{Proof}
-%	  ...				  ...
-%	  \begin{eqnarray}		  \begin{itemize}
-%	   ... &=& ... \\		    \item ...
-%	   ..  &=& ... &\qed		    \item ...   \qed
-%	  \end{eqnarray}		  \end{itemize}
-%	\end{Proof}			\end{Proof}
-% also works with $$...$$ and \[...\] displays, including fleqn.sty.
-
-% Unfortunately some environments, such as picture, do not allow this at all.
-% In fact \qed will only work in those environments which provide access to
-% the right hand side of the page. In other words, wherever you think
-% "\hfill\square" ought to work then \qed will; of course it is just because
-% that naive method doesn't work that this macro file is needed at all.
-% The macro was designed to solve the problem in the case of "unrestricted
-% horizontal mode" (ie at the end of a paragraph); it also works in $$
-% displays by pretending to be an equation number. In most other cases it
-% basically does "\hfill\square" or "\hfill$\square$" and hopes for the best.
-
-% If you have to put \qed outside the environment, it may be appropriate to
-% put \vskip-\baselineskip before it, unless of course this would over-print.
-% There is, however, still a danger that TeX will break the page here.
-
-% The eqnarray example above does not in fact work: if you try it you'll
-% get "! Paragraph ended before \llap was complete" with LaTeX in a mess.
-% This is a very common place where you might want to put the end of proof
-% mark, and I also consider that the fourth column should be available for
-% "reasons" for equational steps.  The following substitute for \eqnarray
-% allows this, whilst being compatible with automatic numbering. I have
-% proposed it to Rainer Sch\"opf for inclusion in LaTeX. If you want to
-% use it, please copy it to another file rather than uncommenting it here.
-% Don't forget to use \makeatletter or put it in a documentstyle (.sty) file.
-%
-% \def\eqnarray{\stepcounter{equation}\let\@currentlabel\theequation
-% \global\@eqnswtrue\m@th\global\@eqcnt\z@\tabskip\@centering\let\\\@eqncr
-% $$\halign to\displaywidth\bgroup\@eqnsel\hskip\@centering$\displaystyle
-% \tabskip\z@{##}$&\global\@eqcnt\@ne\hskip 2\arraycolsep \hfil${##}$\hfil
-% &\global\@eqcnt\tw@\hskip2\arraycolsep$\displaystyle\tabskip\z@{##}$\hfil
-% \tabskip\@centering&%
-%	\global\@eqcnt\thr@@\hbox to\z@\bgroup\hss##%*** instead of "\llap{##}"
-% \tabskip\z@\cr}%
-% \def\@@eqncr{\let\@tempa\relax
-% \ifcase\@eqcnt \def\@tempa{& & &}\or \def\@tempa{& &}%
-%	\or\def\@tempa{&}\else\@eqnswfalse%*** instead of "\else\def\@tempa{&}"
-% \fi\@tempa\if@eqnsw\@eqnnum\stepcounter{equation}\fi
-%	\egroup%*** added, to match \bgroup in fourth cell of preamble
-% \global\@eqnswtrue\global\@eqcnt\z@\cr}
-%
-% More generally, each individual environment (both the standard ones and
-% those defined by the user) needs to co-operate in order to make this work.
-% But it is not the business of this macro to rewrite LaTeX in this way.
-
-% Why can't we do all of this with \endProof? Because by that stage
-% the damage has been done: the environments, paragraphs or
-% displays have already been closed and their \hbox'es added
-% to the current vertical list, and cannot be removed for
-% alteration if this is the current page.
-
-% Even if you don't need to put \qed inside an inner environment
-% to avoid a blank line, it's still a good idea to do so, because
-% otherwise it's possible that intervening end-of-environment
-% material may allow TeX to put the mark on the next page.
-
-% This file may be called QED.sty, QED.tex, qed.sty or qed.tex.
-% It may be loaded either as a \documentstyle option or using \input,
-% as it is careful to handle the \catcode of @ appropriately.
-
-% If you don't use theorem.sty, this file instead provides options to use
-% commands to begin theorems, instead of enclosing them in environments,
-% and to suppress numbering and italicisation. A rudimentary version of
-% \newtheorem for plain TeX is also implemented (always using commands
-% rather than environments).
-
-% At the end of the file some useful \newtheorem
-% commands are listed but not executed.
-
-% \Theorem\Proof\endProof\qed will print the second square, whereas
-% \begin{Theorem}\end{Theorem}\begin{Proof}\end{Proof}\qed will not.
-
-%=========================================================================
-% Make @ letter, saving its old code to restore at the end of this file.
-% Look for this towards the end of the file if you think something's missing!
-% "plain.tex" defines \lq as a synonym for back quote (character constant);
-% I use it to avoid corruption when sending TeX files by email via BITNET.
-\edef\qedrestoreat{\noexpand\catcode\lq\noexpand\@=\the\catcode\lq\@}%%
-\catcode\lq\@=11
-
-% in LaTeX, \protect the user commands;
-% in plain TeX, ensure that it is defined.
-\ifx\protect\undefined\let\protect\relax\fi
-
-%=========================================================================
-
-%				OPTIONS
-
-% These are the user commands.
-
-\def\qed{\protect\@qed{$\qedsymbol$}}% suppressible printing of \qedsymbol
-\def\pushright{\protect\@pushright}% takes an argument, which it always prints
-
-% theoremata in Euclid needed proof:   "which   was  to be shown"
-\def\QED{\protect\@qed{{\rm Q.E.D.}}}% "quod   erat  demonstrandum"
-
-% but problemata needed construction:  "which   was  to be found"
-\def\QEI{\protect\@qed{{\rm Q.E.I.}}}% "quod   erat  inveniendum"
-
-% a LaTeX environment
-\def\Proof{\protect\@Proof}\def\endProof{\protect\@endProof}%
-\let\proof\Proof\let\endproof\endProof
-
-
-% These are the user-settable parameters.
-
-% The actual (maths) symbol used by \qed
-\def\qedsymbol{\square}% PLEASE NOTE: this is in the AMS symbols font.
-%\def\qedsymbol{\blacksquare}%  use one of these instead
-%\def\qedsymbol{\hbox{\rm Q.E.D.}}%        if you prefer
-
-% This is the text used by \Proof.
-% A new paragraph is begun without indentation.
-% Change it to {\kern\parindent\sc D\'emonstration: } if you like.
-\def\TheWordProof{\bf Proof\enskip}
-
-% This is the font command used for the text of proofs
-\def\ProofFont{}
-
-% The command \AutoQEDtrue causes a \qed in \end{Theorem}, so you do
-%	\begin{Theorem} ... \begin{Proof} ... \end{Proof} \end{Theorem}
-% but if you omit the proof, the statement gets a little square at the end.
-\newif\ifAutoQED\AutoQEDfalse
-
-% The remaining options are redundant with theorem.sty
-% so are not defined if this has been loaded.
-\newif\ifNumberResults
-\ifx\theorem@style\undefined
-   %
-   % How to print the name (#1), number (#2) and attribution (#3) of a theorem.
-   \NumberResultstrue
-   % If the number (#2) is absent, "\unskip" removes the
-   % unwanted space "\ " from before it (16 Feb 1993).
-   \def\TheoremHeader#1#2#3{\bf #1\ifNumberResults\ #2\unskip\fi#3}
-   %
-   % This is the font command used for the text of theorem enunciations
-   % change to {\rm} or {\small} if you like.
-   \def\TheoremFont{\it}
-   %
-   % The command \NumberResultsfalse will suppress theorem numbering.
-   %
-   % The command \TheoremsAsCommands will allow you to write
-   % \Theorem instead of \begin{Theorem} ... \end{Theorem}.
-   % In this case italicisation is suppressed by default.
-   % To do this with theorem.sty would involve rewriting the substyles.
-   %
-   % WARNING: if you subsequently redefine \TheoremFont, and use the command
-   % instead of the environment, the font will remain in force afterwards!
-\fi
-
-%=========================================================================
-%  If you already have a macro called \qed, \endproof or \pushright
-%  which is laid out in a similar way to the following two definitions
-%  (but with \hbox@pushright incorporated) then it is almost certainly
-%  my code, which has been copied anonymously via numerous people since
-%  my Cambridge PhD thesis in August 1986. Belated acknowledgements to
-%  Chris Thompson of the Cambridge University Computing Service for his
-%  help with my early attempts at TeX, in particular this problem.
-
-%  The complexity of the macro necessary to get a little box on the
-%  right-hand-side at the end of a proof is amazing.  It really does
-%  have to be this long!  Otherwise you're liable to get it at the
-%  beginning of the next line, or even on the next page. 
-
-\def\parag@pushright#1{{% set up
-    \parfillskip=0pt            % so \par doesnt push \square to left
-    \widowpenalty=10000         % so we dont break the page before \square
-    \displaywidowpenalty=10000  % ditto
-    \finalhyphendemerits=0      % TeXbook exercise 14.32
-    %
-    %                   horizontal
-    %\leavevmode                % not needed since we now only use it in hmode
-    \hbox@pushright		% this used to be incorporated
-    #1%                         % the end-of-proof mark (or whatever)
-    %
-    %                     vertical
-    \par}}%                     % build paragraph with the above parameters
-
-\def\hbox@pushright{% horizontal
-    \unskip                     % remove previous space or glue
-    \nobreak                    % don't break lines
-    \hfil                       % ragged right if we spill over
-    \penalty50                  % discouragement to do so
-    \hskip.2em                  % ensure some space
-    \null                       % anchor following \hfill
-    \hfill                      % push \square to right
-}%
-
-%  Ideally, we would do the above by completing the paragraph, display or
-%  other structure, and then modifying its last line (\hbox).
-%  Unfortunately this cannot be done, because TeX does not allow you to
-%  remove a box (using \lastbox) which has already been contributed to the 
-%  main vertical list (current page).
-
-%  It would, I suppose, be possible to do it by collecting the entire proof
-%  in its own \vbox, modifying that and \unvbox'ing it to the current page.
-%  This approach may lead to the following problems:
-%  (i) overflow of TeX's main memory, especially if the \end{Proof} is missing;
-%  (ii) footnotes, floats, marginpars, labels and index items may be lost.
-%  (iii) I don't know how page-breaking would be handled.
-
-%========================================================================
-
-% Switch to enable/suppress \qedsymbol; since suppression may be done
-% within a nested scope it must be global, so we do our own save/restore
-% in a symbol which is local to the Proof environment.
-% On first use, we check to see whether an obsolete version of Paul.sty
-% is around, and complain loudly if it is, because they interfere seriously.
-
-\newif\if@qed\@qedfalse
-\def\save@set@qed{\check@pt@sty@v\let\saved@ifqed\if@qed\global\@qedtrue}%
-\def\restore@qed{\global\let\if@qed\saved@ifqed}
-
-% prefer proofs with statements if possible - hence \penalty700
-% the only essential part of this is \save@set@qed
-\def\@Proof{%
-   \par\removelastskip\smallskip\penalty700
-   \save@set@qed
-   \noindent\ProofFont{\TheWordProof\enskip}%
-}%
-
-\def\@endProof{%
-   \qed\restore@qed
-   \penalty-700 \smallskip
-}
-
-\def\@qed#1{\check@pt@fm@thm
-\if@qed					% have we already done \qed?
-     \global\@qedfalse\pushright{#1}%  - no  - do it now, but not again
-\else\ifhmode\ifinner\else\par\fi\fi%  - yes - just end paragraph, if any
-\fi}
-
-% \pushright{text} always prints its argument, on the far right, in text mode
-\def\@pushright#1{%
-  \ifvmode				% vertical mode (see comments below)
-       \nobreak				% 22 Feb 1993: don't break page here
-       \null\hfill{#1}\par		% --- #1 alone in a paragraph!
-  \else\ifmmode\maths@pushright{\hbox{#1}}% maths (force a text argument)
-       \else\ifinner\hbox@pushright{#1}%  inside an \hbox
-            \else\parag@pushright{#1}%    in a paragraph
-  \fi  \fi  \fi
-}% (22 Feb 1993) removed extra {} which would destroy our \] below
-
-% In the \hbox and maths cases we are really at the mercy of the environment.
-% Assuming that we have $\qed$ simply embedded in a paragraph, the horizontal
-% processing by \hbox@pushright will at least make sure that the square isn't
-% at the beginning of the line, but we can't stop it being on the next page.
-% However it is more likely that the reason why we're in maths mode is that
-% we're inside an eqnarray or similar, in which case \hfill will do its best
-% to put the square on the right of the available space. (See \vadjust below.)
-\def\maths@pushright#1{%
-  \ifinner
-     \hbox@pushright{#1}%
-  \else
-     \eqno#1%	use TeX's right equation number feature (\eqno) within $$.
-     \def\]{$$\ignorespaces}%	 suppress LaTeX's error checking (HACK!)
-  \fi
-}% (22 Feb 1993) removed extra {} which would destroy our \] above
-
-% An idea that didn't work: see TeXbook p188. (16 Feb 1993)
-% Use \predisplaysize to find out the width of the previous box,
-% in the case where it has already been completed.
-% But this can only be used inside displays ($$), and a display in
-% vertical mode begins a paragraph first, so we end up with
-% \predisplaysize=\parindent+2em whatever happened in the previous
-% paragraph.
-
-% \ifinner is true inside a \vbox or \vadjust; in both of these
-% circumstances we are allowed to remove boxes with \lastbox etc.
-% Maybe it's worth testing this case and doing it.
-
-% Another idea: it may be worth trying \vadjust, if only to insert \nobreak.
-% The problem with this is that if we are too deeply nested in horizontal
-% or maths lists, the adjustment may not be able to find its way out to the
-% enclosing vertical list. In the case of array-like environments, it will
-% appear (assuming it manages to get out) after the current row of the array.
-
-%===========================================================================
-% We have to add to the theorem environments the commands to enable \qed.
-% This is done by re-defining \@thm#1#2.
-% Note that Mittelbach's theorem.sty re-defines \@thm and \@endtheorem, so
-% that must be loaded before us, otherwise our changes will get over-written
-% and \qed will never be enabled.
-% Paul.sty didn't use this method of gaining control inside a theorem,
-% whereas it did define \qed and \pushright, so here is the one place
-% where we can check for it.
-
-\ifx\nonqed@thm\undefined % otherwise double loading causes a loop 22 Feb 1993
-   \let\nonqed@thm\@thm % save original
-   \let\nonqed@endthm\@endtheorem
-\fi
-
-\def\@thm{\save@set@qed\nonqed@thm}%
-\def\@endtheorem{\ifAutoQED\qed\fi\restore@qed\nonqed@endthm}%
-
-%===========================================================================
-% Check for obsolete versions and clashes of this and other macro files.
-% Why do I do this? Because of those people who complain to me that
-% something doesn't work but refuse to read the manual, and those
-% who refuse to update their software, and then publish papers with
-% commutative diagrams full of the bugs which I fixed several years ago.
-
-\def\obsolete@pt@version#1{\errhelp={%
-%     *****************************************************************
-%     *            The master version is available by                 *
-        Anonymous FTP theory.doc.ic.ac.uk /tex/contrib/Taylor/tex/#1}%*
-%     *****************************************************************
-\errmessage{You have an obsolete version of #1 - please get a new one}}%
-
-% First check QED.sty
-\ifnum\year>1993 \obsolete@pt@version{QED.sty}\fi
-
-% If theorem.sty hasn't been loaded, arrange to check it again in \@qed.
-% And check (then) whether you've actually defined \square.
-% changed 2 June 1993: don't define it now, as that would confuse amssymb.sty
-\ifx\theorem@style\undefined
-   \def\check@pt@fm@thm{\relax
-     \ifx\square\undefined
-       \gdef\square{\bigcirc
-          \errhelp={Anonymous ftp e-math.ams.com /ams/amsfonts}%
-          \errmessage{\string\square\space is an AMS symbol}%
-          \global\let\square\bigcirc}%
-     \fi
-      \ifx\theorem@style\undefined
-          \global\let\check@pt@fm@thm\relax
-      \else\errhelp={The macros \@thm and \@endtheorem need to be re-defined.}%
-          \errmessage{QED.sty must be loaded AFTER theorem.sty but before
-           using \string\newtheorem}%
-      \fi
-      \global\let\check@pt@fm@thm\relax
-      }%
-\else
-   \def\check@pt@fm@thm{%
-      \ifx\square\undefined
-         \def\square{\bigcirc
-         \errhelp={Anonymous ftp e-math.ams.com /ams/amsfonts}%
-         \errmessage{\string\square\space is an AMS symbol}%
-         \global\let\square\bigcirc}%
-      \fi
-      \global\let\check@pt@fm@thm\relax
-      }%
-\fi
-
-% Check for Paul.sty, which SERIOUSLY conflicts with this file.
-% and also for version 2 or version 3 of commutative diagrams.
-\def\check@pt@sty@v{%
-   \relax
-   \ifx\@@begintheorem\undefined
-   \else\message{*** QED.sty and the old Paul.sty seriously conflict! ***}%
-        \obsolete@pt@version{Paul.sty}%
-   \fi
-   \ifx\execHorizontalMap\undefined
-        \gdef\obsolete@pt@version##1{}%
-   \else\global\let\di@gr@m\diagram
-        \gdef\diagram{\obsolete@pt@version{diagrams.tex}\di@gr@m}%
-   \fi
-   \global\let\check@pt@sty@v\relax
-}%
-
-
-%===========================================================================
-% If Mittelbach's theorem.sty is loaded, skip the rest of the file.
-\ifx\theorem@style\undefined\else\qedrestoreat\expandafter\endinput\fi
-%===========================================================================
-
-% Allow the user to suppress italicisation and numbering.
-
-% The following two macros are called by LaTeX to begin a theorem
-% respectively with and without an optional (``attribution'') argument.
-% It is clear from latex.tex that they are intended to be customised.
-% The code common to the two has been taken out as \begin@theorem and
-% \TheoremHeader. Of these, the former is re-defined by \TheoremsAsCommands.
-
-\def\@opargbegintheorem#1#2#3{\begin@theorem{\TheoremHeader{#1}{#2}{ (#3)} }}
-
-\def\@begintheorem#1#2{\begin@theorem{\TheoremHeader{#1}{#2}{} }}
-
-\def\begin@theorem#1{%
-  \trivlist\item[\hskip\labelsep {#1}]%		% LaTeX likes this method.
-  \TheoremFont					% Italicise the enunciation
-  \ifx\ProofFont\empty\def\ProofFont{\rm}\fi	% but not any nested proof.
-  }%
-
-
-%%% Here's what LaTeX (92/1/14) does:
-%%%% RmS 91/08/14 Moved \it after \item to make it work with NFSS
-%%\def\@begintheorem#1#2{\trivlist \item[\hskip \labelsep{\bf #1\ #2}]\it}
-%%\def\@opargbegintheorem#1#2#3{\trivlist
-%%      \item[\hskip \labelsep{\bf #1\ #2\ (#3)}]\it}
-%%\def\@endtheorem{\endtrivlist}
-
-
-% The document style option "theorems-as-commands" will allow you to
-% write \Theorem instead of \begin{Theorem} ... \end{Theorem}.
-\def\TheoremsAsCommands{%
-  \def\TheoremFont{}% suppress italicised theorems.
-  \def\begin@theorem##1{%
-     \par\removelastskip\smallskip
-     \save@set@qed % enable \qed
-     \noindent{##1}% the name
-     \TheoremFont % italicise at your own risk!
-   }%
-  \def\@endtheorem{\ifAutoQED\qed\fi\restore@qed}%
-}%
-
-\expandafter\let\csname ds@theorems-as-commands\endcsname\TheoremsAsCommands
-
-%===========================================================================
-% If we're running under LaTeX, skip the rest of the file.
-\ifx\newtheorem\undefined\else\qedrestoreat\expandafter\endinput\fi
-%===========================================================================
-
-% This implements a rudimentary version of \newtheorem for plain TeX.
-% Only the unattributed theorems and the
-% declarations \newtheorem{Theorem}[Result]{Theorem} and
-% \newtheorem{Convention}[Unnumbered]{Convention} are supported.
-% The numbering is based on the counts \chapternumber, \sectionnumber
-% and \subsectionnumber, which it is up to you to define with \newcount.
-% It's also up to you to reset \c@Result at the beginning of each section.
-
-% Form the number: (chapter).(section).(subsection).(#1)
-% where any of the first three parts which is zero
-% negative or undefined is omitted.
-\def\ther@sult#1{%
-\ifx\chapternumber\undefined\else
-   \ifnum\chapternumber>0 \number\chapternumber.\fi\fi
-\ifx\sectionnumber\undefined\else
-   \ifnum\sectionnumber>0 \number\sectionnumber.\fi\fi
-\ifx\subsectionnumber\undefined\else
-   \ifnum\subsectionnumber>0 \number\subsectionnumber.\fi\fi
-\expandafter\number\csname c@#1\endcsname}%
-
-% plain version of LaTeX's \@thm
-\def\plain@thm#1#2{% #1=counter, #2=text
-  \save@set@qed
-  \expandafter\advance\csname c@#1\endcsname1
-  \@begintheorem{#2}{\csname the#1\endcsname}%
-}%
-
-% Rudimentary \newtheorem
-\def\newtheorem#1[#2]#3{%   #1=command, #2=counter, #3=text
-  %
-  % \def\#1{\plain@thm{#2}{#3}}
-  \expandafter\def\csname #1\endcsname{\plain@thm{#2}{#3}}%
-  %
-  % \def\end#1{\@endtheorem}
-  \expandafter\def\csname end#1\endcsname{\@endtheorem}%
-  %
-  % if \c@#2 is not defined
-  %    \newcount\c@#2
-  %    \def\the#2{\ther@sult{#2}}
-  \expandafter\ifx\csname c@#2\endcsname\relax
-     \expandafter\expandafter\csname newcount\endcsname
-        \csname c@#2\endcsname
-     \expandafter\def\csname the#2\endcsname{\ther@sult{#2}}%
-  \fi
-}%
-
-\TheoremsAsCommands
-
-\qedrestoreat\endinput
-
-%===========================================================================
-
-% The following commands are not executed (because of \endinput above),
-% but you may find it convenient to include some of them.
-
-% First set up uniform numbering in LaTeX;
-% don't use this in plain TeX because this usage of \newcommand is not
-% supported and we have already done by hand what it would do in LaTeX,
-% viz to define the macro \theResult and the count \c@Result.
-\ifx\@@thm\undefined
-	\newtheorem{Result}{Result}[subsection]%
-	\@addtoreset{Result}{section}%
-	\ifx\chapter\undefined\else\@addtoreset{Result}{chapter}\fi
-\fi
-
-\let\theUnnumbered\relax\countdef\c@Unnumbered255 \def\p@Unnumbered{}
-
-\newtheorem{Answer}[Result]{Answer}
-\newtheorem{Answers}[Result]{Answers}
-\newtheorem{Conjecture}[Result]{Conjecture}
-\newtheorem{Construction}[Result]{Construction}
-\newtheorem{Convention}[Unnumbered]{Convention}
-\newtheorem{Corollary}[Result]{Corollary}
-\newtheorem{Counterexample}[Result]{Counterexample}
-\newtheorem{Definition}[Result]{Definition}
-\newtheorem{Example}[Result]{Example}
-\newtheorem{Examples}[Result]{Examples}
-\newtheorem{Exercise}[Result]{Exercise}
-\newtheorem{Exercises}[Result]{Exercises}
-\newtheorem{Fact}[Result]{Fact}
-\newtheorem{Facts}[Result]{Facts}
-\newtheorem{Lemma}[Result]{Lemma}
-\newtheorem{NB}[Unnumbered]{NB}
-\newtheorem{Notation}[Result]{Notation}
-\newtheorem{Note}[Unnumbered]{Note}
-\newtheorem{Observation}[Result]{Observation}
-\newtheorem{Observations}[Result]{Observations}
-\newtheorem{Problem}[Result]{Problem}
-\newtheorem{Proposition}[Result]{Proposition}
-\newtheorem{PS}[Unnumbered]{PS}
-\newtheorem{Remark}[Result]{Remark}
-\newtheorem{Question}[Result]{Question}
-\newtheorem{Questions}[Result]{Questions}
-\newtheorem{Theorem}[Result]{Theorem}
-\newtheorem{Thesis}[Result]{Thesis}
-\newtheorem{Warning}[Result]{Warning}
-
diff --git a/Master/texmf-dist/source/latex/proofs/taylor/QED.sty b/Master/texmf-dist/source/latex/proofs/taylor/QED.sty
deleted file mode 100644
index bdf443cee19..00000000000
--- a/Master/texmf-dist/source/latex/proofs/taylor/QED.sty
+++ /dev/null
@@ -1,731 +0,0 @@
-\message{<Paul Taylor's right-justified end-of-proof mark, 24 June 1995>}
-%%========================================================================
-%************************************************************************%
-%*                                                                      *%
-%*      Maybe you already have a \qed macro to put a little square      *%
-%*      on the right hand side at the end of a mathematical proof?      *%
-%*                                                                      *%
-%*                      IT'S PROBABLY MINE!                             *%
-%*                                                                      *%
-%*           Please compare yours with \parag@pushright below.          *%
-%*                                                                      *%
-%*      This new file is compatible, it fixes the bugs, has extra       *%
-%*      features, and is maintained and portable.  Please use it!       *%
-%*                                                                      *%
-%*      NEW FEATURE \WillHandleQED and \HandleQED for environments      *%
-%*      which do not give access to the right hand side of the page.    *%
-%*                                                                      *%
-%*      Now also available: \DefineStandardTheorems or                  *%
-%*      \usepackage[define-standard-theorems]{QED}                      *%
-%*                                                                      *%
-%************************************************************************%
-%========================================================================%
-
-% COPYRIGHT (C) 1993-6 Paul Taylor, Department of Computer Science,
-% Queen Mary & Westfield College, London E1 4NS.
-% You may use this file for any purpose. You may copy it on condition that
-% you do so in exactly the form in which it was supplied, make no charge
-% for the copy and impose the same conditions on the recipient.
-% This software is supplied ``as is'' without warranty, express or implied,
-% including but not limited to merchantability and fitness for any particular
-% purpose. No liability is accepted by the author, Queen Mary and Westfield
-% College, Imperial College or any third party for any direct or consequential
-% damages, however caused.
-% In all cases you must keep several backup versions of your files in a place
-% to which your machine cannot write, and you must check documents visually
-% before submitting the final version to a publisher or expensive printer.
-
-% WARNING: If you use this with Frank Mittlebach's "theorem.sty" you
-% MUST load theorem first, then QED, then do the \newtheorem commands.
-
-%       Authoritative version:  /pub/tex/contrib/pt/proofs/QED.sty
-%       by anonymous FTP from:  ftp.dcs.qmw.ac.uk
-%       also CTAN:              macros/generic/proofs/taylor/QED.sty
-%       author/maintained by:   Dr Paul Taylor <pt@dcs.qmw.ac.uk>
-
-% WARNING: This file replaces some of the functions of "Paul.sty"
-% and MUST NOT be used with it as serious conflicts will arise.
-
-%=========================================================================
-
-%       USER INTERFACE AND EXAMPLES (see also OPTIONS below)
-
-% LaTeX2e \usepackage options: see \DeclareOption commands below
-% theorems-as-commands roman-theorems italic-theorems
-% auto-QED explicit-QED number-theorems dont-number-theorems
-% black-square open-square
-
-%       \begin{Proof} ... \end{Proof}
-%       or    \Proof  ... \endProof
-%       or    \Proof  ... \endproof
-%       or    \Proof  ... \qed          also \QED \QEF and \QEI
-
-% WARNING: \qed which doesn't follow \Proof will not print the square.
-
-% Each properly nested Proof/endProof pair gets a single
-% \qedsymbol at the end, on the far right hand side.
-% Unfortunately, this may still be in the wrong place
-% if the proof ends with a display or itemisation.
-% To solve this, \qed may be put *inside* the last substantive
-% environment; the \qedsymbol will be put at that point
-% (the visual end) and suppressed at the logical end of proof.
-
-% Examples:
-%       \begin{Proof}                   \begin{Proof}
-%         ...                             ...
-%         \begin{eqnarray}                \begin{itemize}
-%          ... &=& ... \\                   \item ...
-%          ..  &=& ... &\qed                \item ...   \qed
-%         \end{eqnarray}                  \end{itemize}
-%       \end{Proof}                     \end{Proof}
-% also works with $$...$$ and \[...\] displays, including fleqn.sty.
-
-% Unfortunately some environments, such as picture, do not allow this at all.
-% See the section "centering environments" below for the mechanism for
-% passing \qed to such an environment for special processing.
-
-% In fact \qed will only work in those environments which provide access to
-% the right hand side of the page. In other words, wherever you think
-% "\hfill\square" ought to work then \qed will; of course it is just because
-% that naive method doesn't work that this macro file is needed at all.
-% The macro was designed to solve the problem in the case of "unrestricted
-% horizontal mode" (ie at the end of a paragraph); it also works in $$
-% displays by pretending to be an equation number. In most other cases it
-% basically does "\hfill\square" or "\hfill$\square$" and hopes for the best.
-
-% If you have to put \qed outside the environment, it may be appropriate to
-% put \vskip-\baselineskip before it, unless of course this would over-print.
-% There is, however, still a danger that TeX will break the page here.
-% This seems to be unavoidable if the environment ends with a \penalty.
-
-% The eqnarray example above does not in fact work: if you try it you'll
-% get "! Paragraph ended before \llap was complete" with LaTeX in a mess.
-% This is a very common place where you might want to put the end of proof
-% mark, and I also consider that the fourth column should be available for
-% "reasons" for equational steps.  The following substitute for \eqnarray
-% allows this, whilst being compatible with automatic numbering. I have
-% proposed it to Rainer Sch\"opf for inclusion in LaTeX. If you want to
-% use it, please copy it to another file rather than uncommenting it here.
-% Don't forget to use \makeatletter or put it in a documentstyle (.sty) file.
-%
-% \def\eqnarray{\stepcounter{equation}\let\@currentlabel\theequation
-% \global\@eqnswtrue\m@th\global\@eqcnt\z@\tabskip\@centering\let\\\@eqncr
-% $$\halign to\displaywidth\bgroup\@eqnsel\hskip\@centering$\displaystyle
-% \tabskip\z@{##}$&\global\@eqcnt\@ne\hskip 2\arraycolsep \hfil${##}$\hfil
-% &\global\@eqcnt\tw@\hskip2\arraycolsep$\displaystyle\tabskip\z@{##}$\hfil
-% \tabskip\@centering&%
-%       \global\@eqcnt\thr@@\hbox to\z@\bgroup\hss##%*** instead of "\llap{##}"
-% \tabskip\z@\cr}%
-% \def\@@eqncr{\let\@tempa\relax
-% \ifcase\@eqcnt \def\@tempa{& & &}\or \def\@tempa{& &}%
-%       \or\def\@tempa{&}\else\@eqnswfalse%*** instead of "\else\def\@tempa{&}"
-% \fi\@tempa\if@eqnsw\@eqnnum\stepcounter{equation}\fi
-%       \egroup%*** added, to match \bgroup in fourth cell of preamble
-% \global\@eqnswtrue\global\@eqcnt\z@\cr}
-
-% Why can't we do all of this with \endProof? Because by that stage
-% the damage has been done: the environments, paragraphs or
-% displays have already been closed and their \hbox'es added
-% to the current vertical list, and cannot be removed for
-% alteration if this is the current page.
-
-% Even if you don't need to put \qed inside an inner environment
-% to avoid a blank line, it's still a good idea to do so, because
-% otherwise it's possible that intervening end-of-environment
-% material may allow TeX to put the mark on the next page.
-
-% This file may be called QED.sty, QED.tex, qed.sty or qed.tex.
-% It may be loaded using \input, \usepackage or as a \documentstyle option,
-% as it is careful to handle the \catcode of @ appropriately.
-
-% If you don't use theorem.sty, this file instead provides options to use
-% commands to begin theorems, instead of enclosing them in environments,
-% and to suppress numbering and italicisation. A rudimentary version of
-% \newtheorem for plain TeX is also implemented (always using commands
-% rather than environments).
-
-% At the end of the file some useful \newtheorem
-% commands are listed but not executed.
-
-% NB \Theorem\Proof\endProof\qed will print the second square, whereas
-% \begin{Theorem}\end{Theorem}\begin{Proof}\end{Proof}\qed will not.
-
-%=========================================================================
-% Make @ letter, saving its old code to restore at the end of this file.
-% Look for this towards the end of the file if you think something's missing!
-% "plain.tex" defines \lq as a synonym for back quote (character constant);
-% I use it to avoid corruption when sending TeX files by email via BITNET.
-\edef\qedrestoreat{\noexpand\catcode\lq\noexpand\@=\the\catcode\lq\@}%%
-\catcode\lq\@=11
-
-% in LaTeX, \protect the user commands;
-% in plain TeX, ensure that it is defined.
-\ifx\protect\undefined\let\protect\relax\fi
-
-%=========================================================================
-
-%                               OPTIONS
-
-% These are the user commands.
-
-\def\qed{\protect\@qed{$\qedsymbol$}}% suppressible printing of \qedsymbol
-% \pushright takes an argument, which it always prints
-% it is (re)defined by \WillHandleQED and \UnHandleQED below (12.4.94)
-
-% theoremata in Euclid needed proof:    "which   was  to be shown"
-\def\QED{\protect\@qed{{\rm Q.E.D.}}}%  "quod   erat  demonstrandum"
-
-% but problemata needed construction:   "which   was  to be found"
-\def\QEI{\protect\@qed{{\rm Q.E.I.}}}%  "quod   erat  inveniendum"
-
-% alternatively:                        "which   was  to be done/made"
-\def\QEF{\protect\@qed{{\rm Q.E.F.}}}%  "quod   erat  faciendum"
-
-% a LaTeX environment
-\def\Proof{\protect\@Proof}\def\endProof{\protect\@endProof}%
-\let\proof\Proof\let\endproof\endProof
-
-
-% These are the user-settable parameters.
-
-% The actual (maths) symbol used by \qed
-\def\qedsymbol{\square}% PLEASE NOTE: this is in the AMS symbols font.
-%\def\qedsymbol{\blacksquare}%  use one of these instead
-%\def\qedsymbol{\hbox{\rm Q.E.D.}}%        if you prefer
-%\def\qedsymbol{\dashv}% this is what the Journal of Symbolc Logic likes.
-
-% This is the text used by \Proof.
-% A new paragraph is begun without indentation.
-% Change it to {\kern\parindent\sc D\'emonstration: } if you like.
-\def\TheWordProof{\bf Proof\enskip}
-
-% This is the font command used for the text of proofs
-\def\ProofFont{}
-
-% The command \AutoQEDtrue causes a \qed in \end{Theorem}, so you do
-%       \begin{Theorem} ... \begin{Proof} ... \end{Proof} \end{Theorem}
-% but if you omit the proof, the statement gets a little square at the end.
-\newif\ifAutoQED\AutoQEDfalse
-
-% The remaining options are redundant with theorem.sty
-% so are not defined if this has been loaded.
-\newif\ifNumberResults
-\ifx\theorem@style\undefined
-   %
-   % How to print the name (#1), number (#2) and attribution (#3) of a theorem.
-   \NumberResultstrue
-   % If the number (#2) is absent, "\unskip" removes the
-   % unwanted space "\ " from before it (16 Feb 1993).
-   \def\TheoremHeader#1#2#3{\bf #1\ifNumberResults\ #2\unskip\fi#3}
-   %
-   % This is the font command used for the text of theorem enunciations
-   % change to {\rm} or {\small} if you like.
-   \def\TheoremFont{\it}
-   %
-   % The command \NumberResultsfalse will suppress theorem numbering.
-   %
-   % The command \TheoremsAsCommands will allow you to write
-   % \Theorem instead of \begin{Theorem} ... \end{Theorem}.
-   % In this case italicisation is suppressed by default.
-   % To do this with theorem.sty would involve rewriting the substyles.
-   %
-   % WARNING: if you subsequently redefine \TheoremFont, and use the command
-   % instead of the environment, the font will remain in force afterwards!
-\fi
-
-% The document style option "theorems-as-commands" will allow you to
-% write \Theorem instead of \begin{Theorem} ... \end{Theorem}.
-% Moved here from further down. 10 Jan 1994
-\def\TheoremsAsCommands{%
-  \def\TheoremFont{}% suppress italicised theorems.
-  \def\begin@theorem##1{%
-     \par\removelastskip\smallskip
-     \save@set@qed % enable \qed
-     \noindent{##1}% the name
-     %\TheoremFont % italicise at your own risk!
-   }%
-  \def\@endtheorem{\ifAutoQED\qed\fi\restore@qed}%
-}%
-
-\expandafter\let\csname ds@theorems-as-commands\endcsname\TheoremsAsCommands
-
-%=========================================================================
-%  If you already have a macro called \qed, \endproof or \pushright
-%  which is laid out in a similar way to the following two definitions
-%  (but with \hbox@pushright incorporated) then it is almost certainly
-%  my code, which has been copied anonymously via numerous people since
-%  my Cambridge PhD thesis in August 1986. Belated acknowledgements to
-%  Chris Thompson of the Cambridge University Computing Service for his
-%  help with my early attempts at TeX, in particular this problem.
-
-%  The complexity of the macro necessary to get a little box on the
-%  right-hand-side at the end of a proof is amazing.  It really does
-%  have to be this long!  Otherwise you're liable to get it at the
-%  beginning of the next line, or even on the next page. 
-
-\def\parag@pushright#1{{% set up
-    \parfillskip=0pt            % so \par doesnt push \square to left
-    \widowpenalty=10000         % so we dont break the page before \square
-    \displaywidowpenalty=10000  % ditto
-    \finalhyphendemerits=0      % TeXbook exercise 14.32
-    %
-    %                   horizontal
-    %\leavevmode                % not needed since we now only use it in hmode
-    \hbox@pushright             % this used to be incorporated
-    #1%                         % the end-of-proof mark (or whatever)
-    %
-    %                     vertical
-    \par}}%                     % build paragraph with the above parameters
-
-\def\hbox@pushright{% horizontal
-    \unskip                     % remove previous space or glue
-    \nobreak                    % don't break lines
-    \hfil                       % ragged right if we spill over
-    \penalty50                  % discouragement to do so
-    \hskip.2em                  % ensure some space
-    \null                       % anchor the following \hfill
-    \hfill                      % push \square to right
-}%
-
-% Ideally \endProof should do all this. We should be able to add the symbol
-% to the last line after the paragraph, display or whatever other structure
-% has been completed and we've returned to vertical mode. This isn't possible
-% on the current page (outer vmode) because \lastbox doesn't work there.
-
-% But \ifinner is true inside a \vbox, \vadjust or \insert (LaTeX \parbox,
-% minipage, figure or table), and in these circumstances we can use \lastbox.
-% We would have to strip & restore glue & penalties (\insert, \mark and \write
-% are obstacles to this) to get access to the last line (box), which may
-% still not have the correct baseline. We could check its natural width
-% against the page width, but if we re-set it, centering and (right)
-% justification might be disturbed. Is this worth the trouble?
-\def\vbox@pushright#1{\expandafter\message %  (2 Jan 1994)
-  {QED.sty could be improved in this case (line \the\inputlineno): please ask}%
-  \page@pushright{#1}}%
-
-% Using this method the Proof environment could be implemented by collecting
-% the entire proof in its own \vbox, modifying that and \unvbox'ing it to the
-% current page. This approach may lead to the following problems:
-%   (i) footnotes, floats, marginpars, labels and index items may be lost;
-%  (ii) overflow of TeX's main memory, especially if \end{Proof} is missing;
-% (iii) I don't know how page-breaking would be handled.
-
-%========================================================================
-
-% Switch to enable/suppress \qedsymbol; since suppression may be done
-% within a nested scope it must be global, so we do our own save/restore
-% in a symbol which is local to the Proof environment.
-% On first use, we check to see whether an obsolete version of Paul.sty
-% is around, and complain loudly if it is, because they interfere seriously.
-
-\newif\if@qed\@qedfalse
-\def\save@set@qed{\check@pt@sty@v\let\saved@ifqed\if@qed\global\@qedtrue}%
-\def\restore@qed{\global\let\if@qed\saved@ifqed}
-
-% prefer proofs with statements if possible - hence \penalty700
-% the only essential part of this is \save@set@qed
-\def\@Proof{%
-   \par\removelastskip\smallskip\penalty700
-   \save@set@qed
-   \noindent\ProofFont{\TheWordProof\enskip}%
-}%
-
-\def\@endProof{%
-   \qed\restore@qed
-   \penalty-700 \smallskip
-}
-
-\def\@qed#1{\check@pt@fm@thm
-\if@qed                                 % have we already done \qed?
-     \global\@qedfalse\pushright{#1}%  - no  - do it now, but not again
-\else\ifhmode\ifinner\else\par\fi\fi%  - yes - just end paragraph, if any
-\fi}
-
-% \pushright{text} always prints its argument, on the far right, in text mode
-\def\@pushright#1{%
-  \ifvmode
-       \ifinner\vbox@pushright{#1}% vertical mode (see comments above)
-       \else   \page@pushright{#1}%
-       \fi
-  \else\ifmmode\maths@pushright{\hbox{#1}}% maths (force a text argument)
-       \else\ifinner\hbox@pushright{#1}%  inside an \hbox
-            \else\parag@pushright{#1}%    in a paragraph
-  \fi  \fi  \fi
-}% (22 Feb 1993) removed extra {} which would destroy our \] below
-
-% In the \hbox and maths cases we are really at the mercy of the environment.
-% Assuming that we have $\qed$ simply embedded in a paragraph, the horizontal
-% processing by \hbox@pushright will at least make sure that the square isn't
-% at the beginning of the line, but we can't stop it being on the next page.
-% However it is more likely that the reason why we're in maths mode is that
-% we're inside an eqnarray or similar, in which case \hfill will do its best
-% to put the square on the right of the available space. (See \vadjust below.)
-\def\maths@pushright#1{%
-  \ifinner
-     \hbox@pushright{#1}%
-  \else
-     \eqno#1%   use TeX's right equation number feature (\eqno) within $$.
-     \def\]{$$\ignorespaces}%    suppress LaTeX's error checking (HACK!)
-  \fi
-}% (22 Feb 1993) removed extra {} which would destroy our \] above
-
-% outer vertical mode (the current page)
-% There's very little we can do in these circumstances!
-% Penalties still allow the page to be broken.
-% If the user has put negative glue in, leave it alone. (15 Feb 1994)
-\def\page@pushright#1{% 18 Jan 1994
-  %\unpenalty % ineffective
-  \skip@\lastskip
-  \ifdim\skip@>\z@
-       \unskip    % remove \parskip, but only (15 Feb 1994) if it's positive
-  \else\skip@\z@\relax
-  \fi
-  %\unpenalty % TeX won't let me do this
-  \dimen@\baselineskip
-  \advance\dimen@-\prevdepth            % save \prevdepth to make a strut
-  \nobreak                              % don't break the page here
-  \nointerlineskip
-  \hbox to\hsize{%
-    \setbox\z@\null
-    \ifdim\dimen@>\z@\ht\z@\dimen@\fi   % simulate \baselineskip
-    \box\z@
-    \hfill
-    #1}%
-  \vskip\skip@                  % replace old \parskip
-}%
-
-% An idea that didn't work: see TeXbook p188. (16 Feb 1993)
-% Use \predisplaysize to find out the width of the previous box,
-% in the case where it has already been completed.
-% But this can only be used inside displays ($$), and a display in
-% vertical mode begins a paragraph first, so we end up with
-% \predisplaysize=\parindent+2em whatever happened in the previous
-% paragraph.
-
-% Another idea: it may be worth trying \vadjust, if only to insert \nobreak.
-% The problem with this is that if we are too deeply nested in horizontal
-% or maths lists, the adjustment may not be able to find its way out to the
-% enclosing vertical list. In the case of array-like environments, it will
-% appear (assuming it manages to get out) after the current row of the array.
-
-%===========================================================================
-% We have to add to the theorem environments the commands to enable \qed.
-% This is done by re-defining \@thm#1#2.
-% Note that Mittelbach's theorem.sty re-defines \@thm and \@endtheorem, so
-% that must be loaded before us, otherwise our changes will get over-written
-% and \qed will never be enabled.
-% Paul.sty didn't use this method of gaining control inside a theorem,
-% whereas it did define \qed and \pushright, so here is the one place
-% where we can check for it.
-
-\ifx\nonqed@thm\undefined % otherwise double loading causes a loop 22 Feb 1993
-   \let\nonqed@thm\@thm % save original
-   \let\nonqed@endthm\@endtheorem
-\fi
-
-\def\@thm{\save@set@qed\nonqed@thm}%
-\def\@endtheorem{\ifAutoQED\qed\fi\restore@qed\nonqed@endthm}%
-
-%===========================================================================
-% "CENTERING" ENVIRONMENTS - 
-% those which don't give their contents access to the right hand side
-% of the page, such as center, picture, ...  (12 April 1994)
-
-% Each individual environment (both the standard ones and those defined
-% by the user) needs to co-operate in order to make \qed and \pushright work.
-% It is not the business of this package to rewrite LaTeX in this way,
-% but the following mechanism may be inserted in to other environments.
-%  - put \WillHandleQED in the \begin part of the environment definition;
-%    then if a \qed occurs in the body of the environment it is stored
-%    in \QEDbox until...
-%  - \HandleQED anywhere in the \end part of the environment definition
-%    (even inside dollars, braces or another environment) prints it.
-%
-% For example:
-% \newenvironment{qedpicture}%
-%    {\begin{picture}\WillHandleQED}%
-%    {\put(0,0){\HandleQED}\end{picture}}
-%
-% To make this compatible with *not* loading QED.sty,
-% add the following to macro files which use \WillHandleQED and \HandleQED:
-%   \ifx\WillHandleQED\undefined
-%      \let\WillHandleQED\relax
-%      \let\HandleQED\relax
-%      \let\UnHandleQED\relax % if you use it
-%      \let\QEDbox\voidb@x    % must have \makeatletter here!
-%   \fi
-%
-% \UnHandleQED restores normal processing; this may be useful for
-% the minipage environment, which has its own notion of "right hand side"
-% of the page.
-%
-% The width of the saved \qed is available for testing as \wd\QEDbox
-
-\newbox\qed@box % the box in which to save \qed for special handling
-
-\def\WillHandleQED{\relax
-\ifx\HandleQED\nohandle@qed
-   % no enclosing environment has declared \WillHandleQED
-   \def\pushright{\global\setbox\qed@box\hbox}% \qed will be saved
-   \let\QEDbox\qed@box % point at the right box
-   \def\HandleQED{\unhbox\QEDbox}% print it
-   \aftergroup\check@handle@qed  % check that this really gets done
-\else
-   % an enclosing environment already wants to catch \qed
-   % \HandleQED doesn't print anything - let the saved \qed pass through
-   \let\QEDbox\voidb@x % by pointing at an empty box
-\fi}
-
-\def\nohandle@qed{%
-\errhelp{One of them is missing: see QED.sty.}%
-\errmessage{This environment uses \string\WillHandleQED\space and
-\string\HandleQED\space incorrectly}}
-
-\def\check@handle@qed{\relax
-\ifvoid\qed@box\else\expandafter\nohandle@qed\fi}
-
-\def\UnHandleQED{%
-\let\HandleQED\nohandle@qed
-\let\QEDbox\voidb@x
-\def\pushright{\protect\@pushright}}%
-
-\UnHandleQED
-
-%===========================================================================
-% Check for obsolete versions and clashes of this and other macro files.
-% Why do I do this? Because of those people who complain to me that
-% something doesn't work but refuse to read the manual, and those
-% who refuse to update their software, and then publish papers with
-% commutative diagrams full of the bugs which I fixed several years ago.
-
-\def\obsolete@pt@version#1{\errhelp={%
-%     *****************************************************************
-%     *            The master version is available by                 *
-        Anonymous FTP ftp.dcs.qmw.ac.uk /pub/tex/contrib/pt/tex/#1}%*
-%     *****************************************************************
-\errmessage{You have an obsolete version of #1 - please get a new one}}%
-
-% First check QED.sty
-%\ifnum\year>1996 \obsolete@pt@version{QED.sty}\fi
-
-% If theorem.sty hasn't been loaded, arrange to check it again in \@qed.
-% And check (then) whether you've actually defined \square.
-% changed 2 June 1993: don't define it now, as that would confuse amssymb.sty
-\ifx\theorem@style\undefined
-   \def\check@pt@fm@thm{\relax
-     \ifx\square\undefined
-       \gdef\square{\bigcirc
-          \errhelp={Anonymous ftp e-math.ams.com /ams/amsfonts}%
-          \errmessage{\string\square\space is an AMS symbol}%
-          \global\let\square\bigcirc}%
-     \fi
-      \ifx\theorem@style\undefined
-          \global\let\check@pt@fm@thm\relax
-      \else\errhelp={The macros \@thm and \@endtheorem need to be re-defined.}%
-          \errmessage{QED.sty must be loaded AFTER theorem.sty but before
-           using \string\newtheorem}%
-      \fi
-      \global\let\check@pt@fm@thm\relax
-      }%
-\else
-   \def\check@pt@fm@thm{%
-      \ifx\square\undefined
-         \def\square{\bigcirc
-         \errhelp={Anonymous ftp e-math.ams.com /ams/amsfonts}%
-         \errmessage{\string\square\space is an AMS symbol}%
-         \global\let\square\bigcirc}%
-      \fi
-      \global\let\check@pt@fm@thm\relax
-      }%
-\fi
-
-% Check for Paul.sty, which SERIOUSLY conflicts with this file.
-% and also for version 2 or version 3 of commutative diagrams.
-\def\check@pt@sty@v{%
-   \relax
-   \ifx\@@begintheorem\undefined
-   \else\message{*** QED.sty and the old Paul.sty seriously conflict! ***}%
-        \obsolete@pt@version{Paul.sty}%
-   \fi
-   \ifx\execHorizontalMap\undefined
-        \gdef\obsolete@pt@version##1{}% it's no longer needed
-   \else\global\let\di@gr@m\diagram
-        \gdef\diagram{\obsolete@pt@version{diagrams.tex}\di@gr@m}%
-   \fi
-   \global\let\check@pt@sty@v\relax
-}%
-
-%===========================================================================
-
-% Define some standard ``theorem'' types.
-
-\def\DefineStandardTheorems{%
-%
-% First set up uniform numbering in LaTeX;
-% don't use this in plain TeX because this usage of \newcommand is not
-% supported and we have already done by hand what it would do in LaTeX,
-% viz to define the macro \theResult and the count \c@Result.
-\relax\ifx\@@thm\undefined
-        \newtheorem{Result}{Result}[subsection]%
-        \@addtoreset{Result}{section}%
-        \ifx\chapter\undefined\else\@addtoreset{Result}{chapter}\fi
-\fi
-%
-\let\theUnnumbered\relax\countdef\c@Unnumbered255 \def\p@Unnumbered{}%
-\let\DefineStandardTheorems\relax
-%
-\newtheorem{Answer}[Result]{Answer}%
-\newtheorem{Answers}[Result]{Answers}%
-\newtheorem{Conjecture}[Result]{Conjecture}%
-\newtheorem{Construction}[Result]{Construction}%
-\newtheorem{Convention}[Unnumbered]{Convention}%
-\newtheorem{Corollary}[Result]{Corollary}%
-\newtheorem{Counterexample}[Result]{Counterexample}%
-\newtheorem{Definition}[Result]{Definition}%
-\newtheorem{Example}[Result]{Example}%
-\newtheorem{Examples}[Result]{Examples}%
-\newtheorem{Exercise}[Result]{Exercise}%
-\newtheorem{Exercises}[Result]{Exercises}%
-\newtheorem{Fact}[Result]{Fact}%
-\newtheorem{Facts}[Result]{Facts}%
-\newtheorem{Lemma}[Result]{Lemma}%
-\newtheorem{NB}[Unnumbered]{NB}%
-\newtheorem{Notation}[Result]{Notation}%
-\newtheorem{Note}[Unnumbered]{Note}%
-\newtheorem{Observation}[Result]{Observation}%
-\newtheorem{Observations}[Result]{Observations}%
-\newtheorem{Problem}[Result]{Problem}%
-\newtheorem{Proposition}[Result]{Proposition}%
-\newtheorem{PS}[Unnumbered]{PS}%
-\newtheorem{Remark}[Result]{Remark}%
-\newtheorem{Question}[Result]{Question}%
-\newtheorem{Questions}[Result]{Questions}%
-\newtheorem{Theorem}[Result]{Theorem}%
-\newtheorem{Thesis}[Result]{Thesis}%
-\newtheorem{Warning}[Result]{Warning}%
-}
-
-%===========================================================================
-% Interaction with LaTeX2e (2 Jan 1994)
-
-\ifx\newtheorem\undefined\else\ifx\ProvidesPackage\undefined
-   \message{^^J^^J}%
-   \message{****************************************************************}%
-   \message{! ***** You are using an obsolete implementation of LaTeX ******}%
-   \message{* A new version - called LaTeX2e - has been available from TeX *}%
-   \message{* FTP archives such as ftp.tex.ac.uk, ftp.uni-stuttgart.de and *}%
-   \message{* pip.shsu.edu since December 1993. It incorporates NFSS2 (the *}%
-   \message{* Mittelbach-Schoepf New Font Selection Scheme) but is reverse *}%
-   \message{* compatible with LaTeX versions 2.09 and is now the standard. *}%
-   \message{****************************************************************}%
-   \message{^^J^^J}%
-\else
-   \ProvidesPackage{QED}[1996/06/24 right-justified end-of-proof mark]%
-   %\ProvidesFile{QED.sty}% I don't understand what this is for
-   \DeclareOption{roman-theorems}{\def\TheoremFont{\rm}}%
-   \DeclareOption{italic-theorems}{\def\TheoremFont{\it}}%
-   \DeclareOption{theorems-as-commands}{\TheoremsAsCommands}%
-   \DeclareOption{auto-QED}{\AutoQEDtrue}%
-   \DeclareOption{explicit-QED}{\AutoQEDfalse}%
-   \DeclareOption{number-theorems}{\NumberResultstrue}%
-   \DeclareOption{dont-number-theorems}{\NumberResultsfalse}%
-   \DeclareOption{black-square}{\def\qedsymbol{\blacksquare}}%
-   \DeclareOption{open-square}{\def\qedsymbol{\square}}%
-   \DeclareOption{define-standard-theorems}{\DefineStandardTheorems}%
-   \ProcessOptions
-\fi\fi
-
-%===========================================================================
-% If Mittelbach's theorem.sty is loaded, skip the rest of the file.
-\ifx\theorem@style\undefined\else\qedrestoreat\expandafter\endinput\fi
-%===========================================================================
-
-% Allow the user to suppress italicisation and numbering.
-
-% The following two macros are called by LaTeX to begin a theorem
-% respectively with and without an optional (``attribution'') argument.
-% It is clear from latex.tex that they are intended to be customised.
-% The code common to the two has been taken out as \begin@theorem and
-% \TheoremHeader. Of these, the former is re-defined by \TheoremsAsCommands.
-
-\def\@opargbegintheorem#1#2#3{\begin@theorem{\TheoremHeader{#1}{#2}{ (#3)} }}
-
-\def\@begintheorem#1#2{\begin@theorem{\TheoremHeader{#1}{#2}{} }}
-
-\def\begin@theorem#1{%
-  \trivlist\item[\hskip\labelsep {#1}]%         % LaTeX likes this method.
-  \TheoremFont                                  % Italicise the enunciation
-  \ifx\ProofFont\empty\def\ProofFont{\rm}\fi    % but not any nested proof.
-  }%
-
-
-%%% Here's what LaTeX (92/1/14) does:
-%%%% RmS 91/08/14 Moved \it after \item to make it work with NFSS
-%%\def\@begintheorem#1#2{\trivlist \item[\hskip \labelsep{\bf #1\ #2}]\it}
-%%\def\@opargbegintheorem#1#2#3{\trivlist
-%%      \item[\hskip \labelsep{\bf #1\ #2\ (#3)}]\it}
-%%\def\@endtheorem{\endtrivlist}
-
-
-
-%===========================================================================
-% If we're running under LaTeX, skip the rest of the file.
-\ifx\newtheorem\undefined\else\qedrestoreat\expandafter\endinput\fi
-%===========================================================================
-
-% This implements a rudimentary version of \newtheorem for plain TeX.
-% Only the unattributed theorems and the
-% declarations \newtheorem{Theorem}[Result]{Theorem} and
-% \newtheorem{Convention}[Unnumbered]{Convention} are supported.
-% The numbering is based on the counts \chapternumber, \sectionnumber
-% and \subsectionnumber, which it is up to you to define with \newcount.
-% It's also up to you to reset \c@Result at the beginning of each section.
-
-% Form the number: (chapter).(section).(subsection).(#1)
-% where any of the first three parts which is zero
-% negative or undefined is omitted.
-\def\ther@sult#1{%
-\ifx\chapternumber\undefined\else
-   \ifnum\chapternumber>0 \number\chapternumber.\fi\fi
-\ifx\sectionnumber\undefined\else
-   \ifnum\sectionnumber>0 \number\sectionnumber.\fi\fi
-\ifx\subsectionnumber\undefined\else
-   \ifnum\subsectionnumber>0 \number\subsectionnumber.\fi\fi
-\expandafter\number\csname c@#1\endcsname}%
-
-% plain version of LaTeX's \@thm
-\def\plain@thm#1#2{% #1=counter, #2=text
-  \save@set@qed
-  \expandafter\advance\csname c@#1\endcsname1
-  \@begintheorem{#2}{\csname the#1\endcsname}%
-}%
-
-% Rudimentary \newtheorem
-\def\newtheorem#1[#2]#3{%   #1=command, #2=counter, #3=text
-  %
-  % \def\#1{\plain@thm{#2}{#3}}
-  \expandafter\def\csname #1\endcsname{\plain@thm{#2}{#3}}%
-  %
-  % \def\end#1{\@endtheorem}
-  \expandafter\def\csname end#1\endcsname{\@endtheorem}%
-  %
-  % if \c@#2 is not defined
-  %    \newcount\c@#2
-  %    \def\the#2{\ther@sult{#2}}
-  \expandafter\ifx\csname c@#2\endcsname\relax
-     \expandafter\expandafter\csname newcount\endcsname
-        \csname c@#2\endcsname
-     \expandafter\def\csname the#2\endcsname{\ther@sult{#2}}%
-  \fi
-}%
-
-\TheoremsAsCommands
-
-\qedrestoreat\endinput
-
-%===========================================================================
-% BUGS
-% \item\qed\end{letterlist} puts the square above the item label.
-
-% ! You can't use `\unskip' in vertical mode.
-% from \qed in a paragraph on its own.
diff --git a/Master/texmf-dist/source/latex/proofs/taylor/boxproof-old.tex b/Master/texmf-dist/source/latex/proofs/taylor/boxproof-old.tex
deleted file mode 100644
index e42924bb08d..00000000000
--- a/Master/texmf-dist/source/latex/proofs/taylor/boxproof-old.tex
+++ /dev/null
@@ -1,142 +0,0 @@
-% mangletex (11 May 1992) run at 19:39 BST Monday 29 June 1992
-\message{<Paul Taylor's Proof Boxes, 29 June 1992>}%%  
-%%=======================================================
-%%  There is now a PROTOTYPE proof-box macro mackage for TRIAL only.
-%%  The syntax and implementation may change.
-%%  It is "boxproof.tex" in the TeX system (so just "\input boxproof").
-%%  There are some examples in ~pt/utilities/misctex/proofboxeg.tex and
-%%  proofboxeg1.tex.
-%%  
-%%  Syntax as follows:
-%%  each line is of the form
-%%     <all/exists_variables> <latex_label> \: <formula> \= <reason> \\
-%%  where 
-%%     <all/exists_variables> is something like "x,y" - its for variables
-%%        declared at the beginning of all-intro and exists-elim boxes
-%%     <latex_label> is a command "\label{fred}" which defines "fred" to
-%%        be the label text, which may be used anywhere as "\ref{fred}"
-%%        - see LaTeX book.
-%%     <formula> is the proposition being asserted
-%%     <reason> is "\intro\land(\ref{john},\ref{mary})"
-%%%  note that the parts are separated by "\:", "\=" and "\\"; these correspond
-%%  to "let identifier = expression : type" in a declarative language.
-%%  
-%%  Proof boxes are "wrapped up" as follows:
-%%  the whole proof in "\begin{proofbox}...\end{proofbox}"
-%%  single-column boxes (all-intro, implies-intro, exists-elim) in "\[...\]"
-%%  double-column boxes are of two kinds:
-%%     separate (and-intro) "\(...\*...\)"
-%%     stuck together (or-elim) "\(...\+...\)"
-%%  
-%%%  At the moment you may only have pairs of parallel boxes, and the width is
-%%%  split in two; later there will be options for mutiple boxes and adjustable
-%%  widths.
-%%  
-%%  Comments please.
-%%  
-%%  WARNING: this is for temporary use only at the moment.
-%%=======================================================
-\catcode`\@=11 \let\plaint@bplus\+\let\+\relax\newcount\prooflineinbox
-\newcount\prooflineinnextbox\newcount\prooflinetotal\newcount\pr@@flinetotal
-\newcount\pr@@flinemax\newcount\proofboxesacross\newdimen\prooflinenowidth
-\newdimen\proofboxformulawidth\newdimen\proofboxrulebreadth\newdimen
-\proofboxrulespace\newdimen\proofboxsurround\newdimen\proofboxmargin\newdimen
-\pr@@fboxhadjust\newdimen\proofboxintercol\newif\ifinproofbox\newif
-\ifleftmostproofbox\newif\ifparallelisand\newskip\proofboxlefttabskip\newskip
-\proofboxrighttabskip\newskip\proofboxbaselineskip\def\runningproofline{%
-\number\prooflinetotal}\def\nestedproofline{\ifinproofbox\enclosingproofline.%
-\fi\number\prooflineinbox}\def\enclosingproofline{}\prooflinenowidth=1em
-\proofboxformulawidth=15em \proofboxrulebreadth=.03em \proofboxrulespace=.2em
-\proofboxsurround=.5em \proofboxlefttabskip=1em \proofboxrighttabskip=1em plus
-1 fil \proofboxbaselineskip=1.8em \proofboxmargin=5em \proofboxintercol=3em
-\def\proofboxleftside{\leaders\hrule width\proofboxrulebreadth\vfill}\def
-\proofboxrightside{\leaders\hrule width\proofboxrulebreadth\vfill}\def
-\proofboxorseparator{\leaders\hrule width\proofboxrulebreadth\vfill}\def
-\proofboxtopside{\leaders\vrule height\proofboxrulebreadth depth\z@\hfill}%
-\def\proofboxbottomside{\leaders\vrule height\proofboxrulebreadth depth\z@
-\hfill}\let\theproofline\runningproofline\def\proofboxmakelabel#1{{%
-\ifleftmostproofbox\setbox0=\hbox{\hss\the\scriptfont1 #1}\ifdim\wd0<%
-\prooflinenowidth\setbox0=\hbox to\prooflinenowidth{\unhbox0}\fi\box0 \fi}}%
-\def\proofboxnonumbers{\def\proofboxmakelabel##1{}} \def\proofbox{\global
-\prooflinetotal=0 \ifvmode\else\vtop\fi\bgroup\let\[\intofullpr@@fbox\let\(%
-\intohalfpr@@fbox\let\:\pr@@fboxcolon\let\=\pr@@fboxequals\let\proofbox
-\intofullpr@@fbox\proofboxesacross=1 \pr@@fb@x}\let\pr@@fb@x\csname\let
-\endpr@@fb@x\endcsname\def\endproofbox{\endpr@@fb@x\proofboxmargin\z@\vskip1%
-ex \unvbox9 \vskip1ex \egroup}\def\intofullpr@@fbox{\pr@@ffirst\pr@@fb@x}\def
-\+#1{<"7C#1}\def\outofpr@@fbox{\endpr@@fb@x\z@\z@\endpr@@ffirst
-\proofboxleftside\pr@@fvalign\putpr@@fedge\proofboxleftside\putpr@@f
-\putpr@@fedge\proofboxrightside\endpr@@fvalign}\def\intohalfpr@@fbox{%
-\pr@@ffirst\advance\proofboxformulawidth-\proofboxintercol\advance
-\proofboxformulawidth-\proofboxsurround\divide\proofboxformulawidth2 \pr@@fb@x
-}\def\pr@@fvalign{m}\def\orpr@@ffirst{\endpr@@fb@x\z@{.5\proofboxintercol}%
-\endpr@@ffirst\proofboxleftside\advance\proofboxformulawidth-%
-\proofboxintercol\advance\proofboxformulawidth-\proofboxsurround\divide
-\proofboxformulawidth2 \let\*\orpr@@fmore\let\+\orpr@@fmore\let\]\orpr@@flast
-\let\)\orpr@@flast\let\endproof\orpr@@flast\pr@@fvalign\putpr@@fedge
-\proofboxleftside\putpr@@f\putpr@@forsep\proofboxorseparator\pr@@fb@x}\def
-\putpr@@forsep{o}\def\orpr@@fmore{\endpr@@fb@x{.5\proofboxintercol}{.5%
-\proofboxintercol}\putpr@@f\putpr@@forsep\proofboxorseparator\pr@@fb@x}\def
-\putpr@@fedge{n}\def\orpr@@flast{\endpr@@fb@x{.5\proofboxintercol}\z@
-\putpr@@f\putpr@@fedge\proofboxrightside\endpr@@fvalign}\def\putpr@@f{t}\def
-\endpr@@fvalign{h}\def\andpr@@ffirst{\endpr@@fb@x\z@\z@\endpr@@ffirst
-\proofboxleftside\advance\proofboxformulawidth-\proofboxintercol\advance
-\proofboxformulawidth-\proofboxsurround\divide\proofboxformulawidth2 \let\*%
-\andpr@@fmore\let\+\andpr@@fmore\let\]\andpr@@flast\let\)\andpr@@flast\let
-\endproof\andpr@@flast\pr@@fvalign\putpr@@fedge\proofboxleftside\putpr@@f
-\putpr@@fedge\proofboxrightside\pr@@fboxhadjust=\proofboxintercol\advance
-\pr@@fboxhadjust-\dimen8 \advance\pr@@fboxhadjust-2\dimen2 \pr@@fb@x}\def
-\la@math{a}\def\andpr@@fmore{\endpr@@fb@x\z@\z@\hadjustandpr@@f\putpr@@fedge
-\proofboxleftside\putpr@@f\putpr@@fedge\proofboxrightside\pr@@fboxhadjust=%
-\proofboxintercol\advance\pr@@fboxhadjust-\dimen8 \advance\pr@@fboxhadjust-2%
-\dimen2 \pr@@fb@x}\def\la@ket{r}\def\andpr@@flast{\endpr@@fb@x\z@\z@
-\hadjustandpr@@f\putpr@@fedge\proofboxleftside\putpr@@f\putpr@@fedge
-\proofboxrightside\endpr@@fvalign}\def\hadjustandpr@@f{\advance
-\pr@@fboxhadjust-\dimen6 \ifdim\pr@@fboxhadjust<\proofboxsurround
-\pr@@fboxhadjust=\proofboxsurround\fi\hrule width\pr@@fboxhadjust height\z@
-depth\z@\cr}\def\pr@@fboxcr{\cr}\def\pr@@fboxequals{&}\def\pr@@fboxcolon{&}%
-\ifnum\pr@@fb@x\pr@@fvalign\putpr@@forsep\putpr@@fedge\putpr@@f
-\endpr@@fvalign\endpr@@fb@x<13\let\pr@@fmtb\relax\else\def\pr@@fmtb#1{}\fi
-\def\pr@@ffirst{\omit\prooflineinnextbox=\prooflineinbox\edef
-\enclosingproofline{\theproofline}%% its line label
-\pr@@flinetotal=\prooflinetotal\let\endproofbox\outofpr@@fbox
-\proofboxesacross=1 \let\+\orpr@@ffirst\let\*\andpr@@ffirst\let\)%
-\outofpr@@fbox\let\]\outofpr@@fbox\inproofboxtrue}\def\la@bra{y}\def
-\endpr@@ffirst#1{\setbox0=\vbox{#1}\global\advance\dimen6\wd0 \advance\dimen6%
-\proofboxsurround\hskip\dimen6 plus 1fil \global\count@=\pr@@flinetotal&\omit
-\setbox8=\hbox\bgroup\pr@@flinetotal=\count@\hskip-\dimen6 \pr@@flinemax=%
-\prooflinetotal\global\prooflinetotal=\pr@@flinetotal\leftmostproofboxfalse
-\inproofboxtrue}\def\pr@@fvalign{\valign\bgroup\vfil##&##&##\vfil&##&##\vfil
-\cr}\def\endpr@@fvalign{\vfil&\vfil&\vfil&\vfil&\vfil\cr\egroup\setbox0=%
-\lastbox\setbox0=\vbox{\unvbox0\unskip\setbox5=\lastbox\unskip\setbox4=%
-\lastbox\unskip\setbox3=\lastbox\unskip\setbox2=\lastbox\unskip\setbox1=%
-\lastbox\global\dimen9=\ht5 \global\advance\dimen9\dp5\global\advance\dimen9%
-\ht4\global\advance\dimen9\dp4\global\dimen4=\ht1 \global\advance\dimen4\dp1%
-\global\advance\dimen4\ht2\global\advance\dimen4\dp1}\global\advance\dimen8%
-\dimen2\kern-\dimen8 \global\prooflinetotal=\pr@@flinemax\egroup\dimen0=\dp8
-\advance\dimen0-\dimen4 \vtop{\setbox0=\null\ht0=\dimen4 \dp0=-\dimen4 \box0%
-\nointerlineskip\box8}\ifdim\dimen0<\z@\dimen0\z@\fi\advance\dimen0-\dimen9
-\vadjust{\vskip-\dimen0}&\omit\global\advance\dimen8\proofboxsurround\hskip
-\dimen8 plus 1 fil \cr}\def\putpr@@fedge#1{\span\omit\span\omit\span\omit
-\span\omit\setbox0=\vbox{#1}\global\dimen2=\wd0 \unvbox0\vfil\cr}\def
-\la@displ{e}\def\putpr@@forsep#1{&\multispan3 \setbox0=\vbox{#1}\global\dimen
-2=\wd0 \unvbox0 &\vfil\cr\noalign{\kern-\dimen2}}\def\putpr@@f{\hbox to\dimen
-5{\proofboxtopside}&\advance\dimen4\proofboxrulespace\vskip\dimen4 plus 1fil&%
-\vskip-\dimen4 \unvbox9 \vskip-\dimen9&\advance\dimen9\proofboxrulespace
-\vskip\dimen9 plus 1 fil&\hbox to\dimen5{\proofboxbottomside}\cr}\ifnum
-\pr@@fb@x\la@bra\la@displ\la@math\la@ket\endpr@@fb@x\+A\let\pr@@fytb\relax
-\else\def\pr@@fytb#1{}\fi\def\pr@@fb@x{\global\setbox9=\vtop\bgroup
-\nointerlineskip\global\prooflineinbox=0 \baselineskip=\proofboxbaselineskip
-\tabskip=\z@\let\\\pr@@fboxcr\halign\bgroup\hskip\proofboxrulespace plus 1fil%
-\let\(\la@math\let\[\la@displ\global\advance\prooflineinbox1 \global\advance
-\prooflinetotal1 \edef\@currentlabel{\theproofline}$##\proofboxmakelabel
-\@currentlabel$&\hskip\proofboxlefttabskip\let\(\la@math\let\[\la@displ$%
-\displaystyle##$\hskip\proofboxrighttabskip&\let\(\la@math\let\[\la@displ$##$%
-\hskip\proofboxrulespace plus1fil \cr}\def\endpr@@fb@x#1#2{\crcr\omit\hskip#1
-plus 1 fil&\omit\hskip\proofboxformulawidth plus 1fil&\omit\hskip#2 plus 1fil%
-\cr\egroup\setbox0=\lastbox\unskip\global\dimen5=\wd0 \setbox0=\hbox{\unhbox0%
-\unskip\setbox0=\lastbox\global\dimen8=\wd0\unskip\setbox0=\lastbox\global
-\dimen7=\wd0\unskip\setbox0=\lastbox\global\dimen6=\wd0\unskip}\setbox0=%
-\lastbox\global\dimen9=\dp0 \nointerlineskip\pr@@fytb{\box0}\egroup\global
-\dimen4=\ht9 }\inproofboxfalse\leftmostproofboxtrue\let\la@bra\(\let\la@ket\)%
-\def\la@math{\la@bra\let\)\la@ket}\def\la@displ{\la@bra\displaystyle\let\]%
-\la@ket}\let\+\plaint@bplus\catcode`\@=12
\ No newline at end of file
diff --git a/Master/texmf-dist/source/latex/proofs/taylor/boxproof.tex b/Master/texmf-dist/source/latex/proofs/taylor/boxproof.tex
deleted file mode 100644
index fef01ef661d..00000000000
--- a/Master/texmf-dist/source/latex/proofs/taylor/boxproof.tex
+++ /dev/null
@@ -1,427 +0,0 @@
-% mangletex (11 May 1992) run at 22:09 GMT Monday 08 November 1993
-%%\title		{\TeX\ macros for proof boxes}
-%%\author		{Paul Taylor\\
-%%			Department of Computing,\\
-%%			Imperial College,\\
-%%			London SW7 2BZ\\
-%%			+44 71 589 5111 {\em ext.} 5057\\
-%%			{\tt<pt@doc.ic.ac.uk>}}
-%%\date{8 November 1993}
-%% % to get the provisional user documentation do
-%% % grep ^%% boxproof.tex | sed 's/^%*//' > boxproof-manual.tex
-%%\documentstyle{article}
-%%\input boxproof.tex
-%%\def\meta#1{\mbox{$\langle\hbox{#1}\rangle$}}
-%%\def\macrowitharg#1#2{{\tt\string#1\bra\meta{#2}\ket}}
-%%{\escapechar-1 \xdef\bra{\string\{}\xdef\ket{\string\}}}
-%%\let\subsection\section
-%%\begin{document}
-%%\maketitle
-%%
-%% \subsection{Introduction}
-%% The proof
-%%\begin{proofbox}
-%%  \(\"1"\:\alpha\leftrightarrow\psi(x,\top)\=\\
-%%        \:\Some\beta.\psi(x,\beta)\=\mathsf{total}\\
-%%    \[\exists\beta\kern-1em\:\psi(x,\beta)\\
-%%      \(\:\beta\=\\
-%%        \:\beta=\top\=(*)\\
-%%        \:\psi(x,\!\top)\=\mathsf{subs}\\
-%%        \:\alpha\=\elim\leftrightarrow(\ref{1})\\
-%%      \*\:\alpha\=\\
-%%        \:\psi(x,\!\top)\=\elim\leftrightarrow(\ref{1})\\
-%%        \:\beta=\top\=\mathsf{func}\\
-%%        \:\beta\=(*)\\
-%%      \)\:\alpha=\beta\=\intro\leftrightarrow\\
-%%        \:\psi(x,\alpha)\=\mathsf{subs}\\
-%%    \]  \:\psi(x,\alpha)\=\elim\exists\\
-%%    \*  \:\psi(x,\alpha)\=\\
-%%      \(\:\alpha\=\\
-%%        \:\alpha=\top\=(*)\\
-%%        \:\phi(x,\!\top)\=\mathsf{subs}\\
-%%      \*\:\psi(x,\!\top)\=\\
-%%        \:\alpha=\top\=\mathsf{func}\\
-%%        \:\alpha\=(*)\\
-%%      \)\:\alpha\leftrightarrow\psi(x,\!\top)\=\intro\leftrightarrow\\
-%%%    \)  \:\psi(x,\alpha)\leftrightarrow(\alpha\leftrightarrow\psi(x,\!\top))
-%%          \=\intro\leftrightarrow\\
-%%\end{proofbox}
-%% is produced by
-%%\begin{verbatim}
-%%\begin{proofbox}
-%%  \(\"1"\:\alpha\leftrightarrow\psi(x,\top)\\
-%%        \:\Some\beta.\psi(x,\beta)                      \=\mathsf{total}\\
-%%    \[\exists\beta\kern-1em\:\psi(x,\beta)\\
-%%      \(\:\beta\\
-%%        \:\beta=\top                                    \=(*)\\
-%%        \:\psi(x,\!\top)                                \=\mathsf{subs}\\
-%%        \:\alpha                         \=\elim\leftrightarrow(\ref{1})\\
-%%      \*\:\alpha\\
-%%        \:\psi(x,\!\top)                 \=\elim\leftrightarrow(\ref{1})\\
-%%        \:\beta=\top                                     \=\mathsf{func}\\
-%%        \:\beta\=(*)\\
-%%      \)\:\alpha=\beta                           \=\intro\leftrightarrow\\
-%%        \:\psi(x,\alpha)                                 \=\mathsf{subs}\\
-%%    \]  \:\psi(x,\alpha)                                  \=\elim\exists\\
-%%    \*  \:\psi(x,\alpha)\\
-%%      \(\:\alpha\\
-%%        \:\alpha=\top                                   \=(*)\\
-%%        \:\phi(x,\!\top)                                \=\mathsf{subs}\\
-%%      \*\:\psi(x,\!\top)\\
-%%        \:\alpha=\top                                   \=\mathsf{func}\\
-%%        \:\alpha                                        \=(*)\\
-%%      \)\:\alpha\leftrightarrow\psi(x,\!\top)   \=\intro\leftrightarrow\\
-%%    \)  \:\psi(x,\alpha)\leftrightarrow
-%%          (\alpha\leftrightarrow\psi(x,\!\top)) \=\intro\leftrightarrow\\
-%%\end{proofbox}
-%%\end{verbatim}
-%%
-%%  Syntax as follows:
-%%  each line is of the form
-%%  \begin{center}
-%%     \meta{variables}
-%%     \meta{name}
-%%     \verb/\:/ \meta{formula}
-%%     \verb/\=/ \meta{reason}
-%%     \verb/\-/ \meta{use}
-%%     \verb/\\/
-%%  \end{center}
-%%  where
-%%  \begin{itemize}
-%%  \item \meta{variables} is something like ``$x,y$'' ---
-%%    it's for variables declared at the beginning of $\intro\forall$- and
-%%    $\elim\exists$-boxes.
-%%  \item \meta{name} is a command \verb/\label{fred}/ which
-%%    defines \verb/fred/ to be the label text, which may be used anywhere
-%%    as \verb/\ref{fred}/ --- see {\em The \LaTeX book.}
-%%    Local labels are also available, using \macrowitharg\lbl{name}
-%%    or \verb/\"/\meta{name}\verb/"/; these obey the scoping rules of
-%%    the boxes.
-%%    You may also refer to the previous line as \verb/\ref{-}/.
-%%  \item \meta{formula} is the proposition being asserted.
-%%  \item \meta{reason} is \verb/\intro\land(\ref{john},\ref{mary})/
-%%         or \verb/\elim\forall(\ref{jim})/.
-%%  \item \meta{use} is provided for linear logic, to record the step
-%%%         which uses this one. How this accords with theory I don't yet know.
-%%  \end{itemize}
-%%  Note that the parts are separated by \verb/\:/, \verb/\=/ and \verb/\\/;
-%%  these correspond to
-%%  \begin{center}
-%%     {\bf let } \meta{name} = \meta{expression} : \meta{type}
-%%  \end{center}
-%%  in a declarative language.
-%%  The \verb/\:/, \verb/\=/ and \verb/\-/ fields are optional and may occur
-%%  in any order. If any of them is repeated the last is taken.
-%%  If none of them is present the \meta{variables} field is also ignored.
-%%
-%%  Proof {\em boxes\/} are ``wrapped up'' as follows:
-%%  \begin{itemize}
-%%%  \item the whole proof in \verb/\begin{proofbox}/...\verb/\end{proofbox}/;
-%%%  \item single-column boxes ($\intro\forall$, $\intro\imp$, $\elim\exists$),
-%%      in \verb/\[/...\verb/\]/.
-%%  \item multiple-column boxes are of two kinds:
-%%    \begin{itemize}
-%%%     \item separate ($\intro\land$) boxes: \verb/\(/...\verb/\*/...\verb/\)/.
-%%     \item stuck together ($\elim\lor$) boxes:
-%%        \verb/\(/...\verb/\+/...\verb/\)/.
-%%    \end{itemize}
-%%  \end{itemize}
-%%  You may put more than two columns in \verb/\(/...\verb/\)/ and even mix
-%%  the \verb/\+/ and \verb/\*/ separators.
-%%
-%%  The whole proof is enclosed in \verb/\proofbox/...\verb/\endproofbox/
-%%  or \verb/\begin{proofbox}/...\verb/\end{proofbox}/, but the \LaTeX\
-%%  environment form {\em must not\/} be used for nested boxes.
-%%
-%%  If the proof occurs in paragraph mode (ie in vertical or
-%%  unrestricted horizontal mode) then it is set as a display, using the
-%%  full width of the page. Otherwise it uses only the required width.
-%%
-%%  A lot of the internals are potentially configurable, but there is not
-%%  yet a user interface suitable for doing this. This will be provided
-%%  in the next version.
-%%
-%%  This is a {\em prototype\/} proof-box macro package;
-%%  the syntax and implementation may change.
-%%  It is {\tt boxproof.tex} in the \TeX\ system
-%%  (so just \verb/\input boxproof/).
-%%
-%%  There are some examples in
-%%  \verb+~pt/utilities/proofs/proofboxeg.tex+ and
-%%  \verb+proofboxeg1.tex+.
-%%
-%%  The prototype version was begun on 2 August 1991, the new one on
-%%  4 June 1993.
-%%
-%%
-\message{<Paul Taylor's Proof Boxes, 8 November 1993>}\edef\proofboxrestoreat
-{\noexpand\catcode`\noexpand\@\the\catcode`\@}\catcode`\@=11 \count@\year
-\multiply\count@12 \advance\count@\month\ifnum\count@> 23970 \message{ ******
-This is an experimental version - please get an up-to-date one ******}%
-\message{ by anonymous FTP theory.doc.ic.ac.uk /tex/contrib/Taylor/tex/%
-boxproof.tex}\fi\let\pb@A\+\let\+\relax\let\pb@B\(\let\pb@C\)\def\pb@D{\pb@B
-\let\)\pb@C}\def\pb@E{\pb@B\displaystyle\let\]\pb@C}%%
-%% The following are user-settable dimensions.
-%% 
-\newdimen\prooflinenowidth\prooflinenowidth1em \newdimen\proofboxfullwidth
-\newdimen\proofboxleftmargin\proofboxleftmargin3em \newdimen
-\proofboxrightmargin\newdimen\proofboxrulebreadth\proofboxrulebreadth.4pt
-\newdimen\proofboxseparation\proofboxseparation.2em \newdimen
-\proofboxbaselineskip\proofboxbaselineskip4ex %%
-%%
-%% The following are user-accessible numbers.
-%%
-\newcount\proofcolumns\newcount\prooflinetotal\newcount\prooflineinbox%%
-%%
-%% These boxes receive the fields of the proof steps.
-%% They are used in \verb/\proofboxmakeleftcolumn/ {\em etc}.
-%%
-\newbox\proofboxproposition\newbox\proofboxreason\newbox\proofboxuse\newbox
-\proofboxvariables%%
-%% The left-most switch is used by
-%%% \verb/\proofboxmakelabel/ to suppress the label in all but the first column.
-%% On the outside it is true.
-\newif\ifleftmostproofbox\leftmostproofboxtrue%%
-%%
-%% The following are obsolete: they are only included for reverse
-%% compatibility with the prototype version.
-\newdimen\proofboxintercol\newdimen\proofboxsurround\newdimen
-\proofboxformulawidth\newdimen\proofboxmargin\newskip\proofboxlefttabskip
-\newskip\proofboxrighttabskip%%
-%%
-%% \subsection{Redefinable macros}
-%% WARNING: most of these commands will be hidden and replaced with
-%% optional arguments to \verb/\proofbox/ in a future version.
-%% Do not rely on them.
-%%
-%% We provide three different ways of numbering the lines of the proof:
-%% \begin{itemize}
-%% \item \verb/\runningproofline/: a global running sequence (default),
-%% 
-\def\runningproofline{\number\prooflinetotal}%%
-%% \item \verb/\nestedproofline/: a hierarchical system with dots,
-%%
-\def\nestedproofline{\relax\ifx\enclosingproofline\empty\else
-\enclosingproofline{.}\fi\number\prooflineinbox}\def\enclosingproofline{}%%
-%% \item \verb/\nestedproofline/: a fully hierarchical system which
-%% also includes the column number
-%% (\verb/\proof@columns/) as a letter (ASCII quote plus number).
-%%
-\def\proofboxcolumn{\ifnum\proofcolumns>\z@{\count@96\advance\count@
-\proofcolumns\char\count@}\fi}\def\fullynestedproofline{\relax\ifx
-\enclosingproofline\empty\enclosingproofline\proofboxcolumn.\else
-\proofboxcolumn\fi\number\prooflineinbox}%%
-%% \end{itemize}
-%% \verb/\theproofline/ is the default.
-%%
-\let\theproofline\runningproofline%%
-%% The macro \verb/\proofboxmakelabel#1/ is used to print the line label.
-%% We only put it in the leftmost box.
-%% It is printed in small non-ranging Arabic numerals
-%% ({\the\scriptfont1 0123456789}).
-%% Right-justify it in \verb/\prooflinenowidth/ if it will fit,
-%% otherwise let it stick out on the right, {\em i.e.}~left-justify it.
-%%
-\def\proofboxmakelabel#1{{\relax\ifleftmostproofbox\setbox\z@\hbox{\hss\the
-\scriptfont\@ne#1}\ifdim\wd\z@<\prooflinenowidth\setbox\z@\hbox to%
-\prooflinenowidth{\unhbox\z@}\fi\box\z@\quad\fi}}%%
-%% Kill the numbers altogether with \verb/\proofboxnonumbers/.
-%%
-\def\proofboxnonumbers{\def\proofboxmakelabel##1{}}%%
-%% How to make the left column of the proof box:
-%% use the variables field, a space if necessary and the line label.
-%%
-\def\proofboxmakeleftcolumn{\kern\proofboxseparation\hfil\dimen@\wd
-\proofboxvariables\unhbox\proofboxvariables\ifdim\dimen@>\z@\quad\fi
-\proofboxmakelabel\@currentlabel}%%
-%% How to make the middle column of the proof box:
-%% left justify the formula field.
-%%
-\def\proofboxmakemiddlecolumn{\unhbox\proofboxproposition\hfil\quad}%%
-%% How to make the right column of the proof box:
-%% use the reason and use fields.
-%%
-\def\proofboxmakerightcolumn{\box\proofboxreason\box\proofboxuse\hfil\kern
-\proofboxseparation}%%
-%%
-%% Make the four edges of a rectangular box and the separator
-%% between \verb/\+/ columns.
-%%
-\def\proofboxleftside{\leaders\hrule width\proofboxrulebreadth\vfill}\def
-\proofboxrightside{\leaders\hrule width\proofboxrulebreadth\vfill}\def
-\proofboxorseparator{\leaders\hrule width\proofboxrulebreadth\vfill}\def
-\proofboxtopside{\leaders\vrule height\proofboxrulebreadth depth\z@\hfill}%
-\def\proofboxbottomside{\leaders\vrule height\proofboxrulebreadth depth\z@
-\hfill}%%
-%%
-%% Use dotted lines: \verb/\dottedproofbox/.
-%%
-\def\dottedproofbox{\def\proofboxleftside{\leaders\pb@F\vfill} \def
-\proofboxrightside{\leaders\pb@F\vfill} \def\proofboxorseparator{\leaders
-\pb@F\vfill} \def\proofboxtopside{\leaders\pb@F\hfill}\def\proofboxbottomside
-{\leaders\pb@F\hfill}%%
-}\def\pb@F{\vbox to 5pt{\vss\hbox to 5pt{\hss.\hss}\vss}}%%
-%% Leave the boxes open at the bottom: \verb/\openproofbox/
-%%
-\def\openproofbox{\def\proofboxbottomside{\hfill}} %%
-%% \subsection{Miscellaneous logical notations}
-%%
-%% Print the names of the introduction and elimination rules, for example:
-%%  \begin{quote}
-%%     \verb/\elim\forall/ $\elim\forall$ \qquad
-%%     \verb/\intro\land/ $\intro\land$ \qquad
-%%  \end{quote}
-\def\intro#1{{{#1}{\cal I}}}\def\elim#1{{{#1}{\cal E}}}%%
-%% Recall that in \TeX\ the logical connectives and quantifiers are called
-%%  \begin{center}
-%%    \verb/\lor/ $\lor$\quad
-%%    \verb/\land/ $\land$\quad
-%%    \verb/\lnot/ $\lnot$\quad
-%%    \verb/\forall/ $\forall$\quad
-%%    \verb/\exists/ $\exists$
-%%  \end{center}
-%% The following provide macros for the \verb/\implies/ {\em relation\/}
-%% and for the binary {\em operation\/} which yields the abstract
-%% \verb/\implic/ation between formulae.
-%% The point is that \TeX\ spaces them and breaks the lines differently:
-%%  \begin{center}
-%%    \verb/A\implies B/ $A\implies B$\quad{\em versus\/}\quad
-%%    \verb/A\implic B/ $A\implic B$
-%%  \end{center}
-%% There are forward and reverse, single and Double versions.
-%%
-\mathchardef\implies="3221 \mathchardef\impliedby="3220 \mathchardef\Implies=%
-"3229 \mathchardef\Impliedby="3228 \mathchardef\implic="2221 \mathchardef
-\implicby="2220 \mathchardef\Implic="2229 \mathchardef\Implicby="2228 \let
-\imp\to%%
-%% Handle the spacing after a variable (and optionally its type)
-%% bound by a quantifier symbol. For example
-%%  \begin{quote}
-%%    \verb/\All x:X. \phi(x)/\quad prints as\quad $\All x:X.\phi(x)$\quad
-%%     instead of\quad $\forall x:X.\phi(x)$
-%%  \end{quote}
-\def\Quantifier#1#2.{\pb@G{#1}#2::.}\def\pb@G#1#2:#3:#4.{{{#1}{#2}\def\next{#%
-3}\ifx\next\empty{.}\mkern1mu \else\mkern1mu{\colon}\mkern1mu{#3}\mkern.5mu{.%
-}\mkern3mu \fi}}%
-%% We provide some commonly used forms; \verb/\iota/ ($\iota$) is Russell's
-%% description operator and should really be inverted.
-\def\All{\Quantifier\forall}\def\Some{\Quantifier\exists}\def\Function{%
-\Quantifier\lambda}\def\Product{\Quantifier\Pi}\def\Sum{\Quantifier\Sigma}%
-\def\TheOne{\Quantifier\iota}\def\Least{\Quantifier\mu}\def\Greatest{%
-\Quantifier\nu}%%
-%% There are several notations for substitution.
-%% After writing $a[x:=b]$ throughout my book I~thought I~might change to
-%% $[b/x]^*a$.
-%% This macro reads the source in the first form and prints in the second.
-%% If you use it you can, like me, defer the decision about
-%% which notation to use until the final stages, doing
-%% \begin{quote}
-%%    \verb/\renewcommand{\Subst}{\plainsubstitution}/
-%% \end{quote}
-%% if you finally decide on making substitution act on the right.
-%% This is already an improvement on the literal text, because it
-%% automatically enlarges the brackets according to the text inside.
-%% \verb/\Subst/ itself is (following my book)
-%% defined in terms of the action of a context morphism (\verb/\CtxtMor/)
-%% on a term. Again you can do
-%% \begin{quote}
-%%    \verb/\renewcommand{\CtxtMor}{\plaincontextmorphism}/
-%% \end{quote}
-%% for something simpler.
-%% This macro interprets its argument as a comma-separated list
-%% of items in the form $x:=b$, which it switches to $b/x$.
-\def\swappingsubstitution#1[#2]{{\CtxtMor[#2]^*{#1}}}\def
-\swappingcontextmorphism[#1]{{\let\pb@J\empty\left[\pb@H#1,[],\/\right]}}\def
-\pb@H#1,{\def\next{#1}\ifx\next\pb@K\else\pb@J\let\pb@J,\pb@I#1:=:=,%
-\expandafter\pb@H\fi}\def\pb@I#1:=#2:=#3,{{\def\next{#2}\ifx\next\empty\else{%
-#2}/\fi{#1} }}\def\pb@K{[]}\def\Subst{\swappingsubstitution}\def\CtxtMor{%
-\swappingcontextmorphism}%%
-%% The simple versions.
-\def\plainsubstitution#1#2{{#1}{\left[{#2}\right]}}\def\plaincontextmorphism#%
-1{{\left[#1\right]}}\newbox\pb@L\newdimen\pb@T\newdimen\pb@U\newdimen\pb@M
-\newdimen\pb@N\newdimen\pb@O\newdimen\pb@P\newdimen\pb@Q\newdimen\pb@R
-\newdimen\pb@S\def\pb@V#1#2{\relax\ifdim#1<#2\relax#1=#2\relax\fi}\count@
-\year\multiply\count@12 \advance\count@\month\ifnum\count@> 23966 \message{%
-because this one has expired and will no longer work!}\endinput\fi%%
-\def\proofbox{\relax\ifmmode\let\next\pb@a\else\let\next\pb@b\ifhmode\ifinner
-\let\next\pb@a\fi\fi\fi\next\global\prooflinetotal\@ne\boxmaxdepth\maxdimen
-\def\[{\pb@w\pb@f\pb@W}\def\({\pb@w\pb@f\pb@X}\def\proofbox{\[}\let\lbl\pb@y
-\def\"##1"{\pb@y{##1}}\def\:{\pb@v\proofboxproposition\displaystyle}\def\={%
-\pb@v\proofboxreason}\def\-{\pb@v\proofboxuse}\def\\{\pb@w\pb@u}\let\+\pb@c
-\let\*\pb@c\let\]\pb@c\pb@p\pb@s}\def\endproofbox{\pb@q\pb@IA\box\pb@L\egroup
-}\def\pb@W{\let\+\pb@d\let\*\pb@d\def\){\pb@e\[\)}\let\]\pb@Y\proofcolumns\z@
-}\def\pb@X{\proofcolumns\@ne\def\+{\pb@j\pb@l}\def\*{\pb@j\pb@m}\def\]{\pb@e
-\(\]}\let\)\pb@Y}\def\pb@Y{\pb@o\pb@u}\def\pb@a{\hbox\bgroup}\def\pb@b{$$%
-\kern-\displayindent\hbox to\hsize\bgroup\proofboxfullwidth\hsize\aftergroup$%
-\aftergroup$}\def\pb@c{\errmessage{Box proofs: \string\+, \string\*, \string
-\) and \string\] may not be used at the top level}}\def\pb@d{\errmessage{Box
-proofs: enclose \string\+ and \string\* in \string\(\string\), not \string\[%
-\string\]}}\def\pb@e#1#2{\errmessage{Box proofs: \string#1 closed by \string#%
-2}\pb@Y}\def\pb@f#1{\setbox\pb@L\hbox\bgroup#1\let\pb@g\pb@n\let
-\enclosingproofline\@currentlabel\edef\pb@h{\the\prooflinetotal}\let\pb@i
-\pb@h\pb@O\z@\pb@M\z@\pb@N-\maxdimen\pb@P\z@\pb@p\pb@t}\def\pb@j#1{\pb@q\pb@k
-\let\pb@g#1\advance\proofcolumns\@ne\global\prooflinetotal\pb@h
-\leftmostproofboxfalse\pb@p\pb@t}\def\pb@k{\pb@g\pb@V\pb@M{\wd\pb@L}\advance
-\pb@O\wd\pb@L\ifnum\pb@i<\prooflinetotal\edef\pb@i{\the\prooflinetotal}\fi
-\ifdim\pb@N<\dp\pb@L\pb@N\dp\pb@L\pb@P\pb@Q\fi\setbox\z@\hbox{%
-\proofboxtopside}\wd\z@\z@\box\z@\setbox\z@\hbox{\proofboxbottomside}\wd\z@
-\z@\box\z@\kern\pb@R\box\pb@L\kern\pb@S}\def\pb@l{\vtop{\proofboxorseparator}%
-\penalty\thr@@}\def\pb@m{\vtop{\proofboxrightside}\kern\proofboxseparation
-\vtop{\proofboxleftside}\penalty\tw@}\def\pb@n{\pb@T\pb@R\setbox\z@\vtop{%
-\proofboxleftside}\dimen@\wd\z@\advance\pb@T\dimen@\advance\pb@T
-\proofboxseparation\kern-\pb@T\kern\proofboxseparation\box\z@\penalty\@ne}%
-\def\pb@o{\pb@q\pb@k\setbox\z@\vtop{\proofboxrightside}\global\advance\pb@S
-\wd\z@\box\z@\global\advance\pb@S\proofboxseparation\kern\proofboxseparation
-\global\prooflinetotal\pb@i\global\pb@R\pb@T\global\pb@Q\pb@P\ifnum
-\proofcolumns<\@ne\proofcolumns\@ne\fi\penalty\proofcolumns\kern-\pb@M\kern
-\pb@M\kern-\pb@O\kern\pb@O\kern-\pb@S\penalty\@ne\egroup\pb@r}\def\pb@p#1{%
-\setbox\pb@L\vtop\bgroup\baselineskip\proofboxbaselineskip\prooflineinbox\@ne
-\pb@T\z@\pb@U\z@#1\pb@u}\def\pb@q{\pb@w\global\pb@R\pb@T\global\pb@S\pb@U
-\egroup}\def\pb@r{\pb@V\pb@T\pb@R\pb@V\pb@U\pb@S\box\pb@L\prevdepth\pb@Q}\def
-\pb@s{}\def\pb@t{}\def\pb@u{\edef\@currentlabel{\theproofline}\let\label@name
-\@currentlabel\setbox\proofboxproposition\box\voidb@x\setbox\proofboxreason
-\box\voidb@x\setbox\proofboxuse\box\voidb@x\setbox\proofboxvariables\hbox
-\bgroup\let\pb@z\pb@AA\let\pb@w\pb@x$}\def\pb@v#1{$\egroup\setbox#1\hbox
-\bgroup\let\pb@z\pb@AA$}\def\pb@w{$\egroup\global\advance\prooflinetotal\@ne
-\advance\prooflineinbox\@ne\setbox\pb@L\hbox{\setbox\z@\hbox{%
-\proofboxmakeleftcolumn}\global\pb@R\wd\z@\kern-\pb@R\box\z@\hbox{%
-\proofboxmakemiddlecolumn}\setbox\z@\hbox{\proofboxmakerightcolumn}\global
-\pb@S\wd\z@\box\z@\kern-\pb@S\penalty\tw@}\global\pb@Q\dp\pb@L\pb@r}\def\pb@x
-{$\egroup}\def\pb@y#1{\aftergroup\pb@z\expandafter\aftergroup\csname r@#1%
-\endcsname}\def\pb@z#1{\edef#1{{\@currentlabel}{}}\expandafter\pb@@A\string#1%
-\\}\expandafter\def\expandafter\pb@@A\string\r@#1\\{\def\label@name{#1}}\def
-\pb@AA#1{\aftergroup\pb@z\aftergroup#1}\expandafter\def\csname r@-\endcsname{%
-{\previous@label}{}}\dimendef\pb@BA=\@ne\dimendef\pb@CA=\tw@\dimendef\pb@DA=%
-\thr@@\dimendef\pb@EA=4 \dimendef\pb@FA=5 \dimendef\pb@GA=6 \chardef\pb@HA=9
-\def\pb@IA{\pb@GA\proofboxfullwidth\pb@T\proofboxleftmargin\pb@V\pb@T\pb@R
-\advance\pb@GA-\pb@T\pb@U\proofboxrightmargin\pb@V\pb@U\pb@S\advance\pb@GA-%
-\pb@U\pb@V\pb@GA{\wd\pb@L}\pb@JA}\def\pb@JA{\setbox\pb@L\vtop{\unvbox\pb@L
-\loop\skip@\lastskip\unskip\setbox\pb@HA\lastbox\ifhbox\pb@HA\pb@KA\repeat
-\unvbox\pb@L\unskip}}\def\pb@KA{\pb@DA\dp\pb@HA\pb@EA\ht\pb@HA\pb@CA\wd\pb@HA
-\setbox\pb@HA\hbox{\unhbox\pb@HA\count@\lastpenalty\unpenalty\unkern\ifodd
-\count@\pb@LA\else\setbox\thr@@\lastbox\setbox\tw@\lastbox\setbox\@ne\lastbox
-\unkern\hbox to\pb@T{\unhbox\@ne}\hbox to\pb@GA{\unhbox\tw@}\hbox to\pb@U{%
-\unhbox\thr@@}\fi}\dp\pb@HA\pb@DA\ht\pb@HA\pb@EA\setbox\pb@L\vtop{\box\pb@HA
-\nointerlineskip\vskip\skip@\unvbox\pb@L}}\def\pb@LA{\pb@O\lastkern\unkern
-\unkern\pb@M\lastkern\unkern\unkern\proofcolumns\lastpenalty\unpenalty\pb@FA
-\pb@T\ifnum\@ne=\proofcolumns\let\pb@MA\pb@NA\else\advance\pb@GA-\pb@CA\pb@BA
-\pb@GA\advance\pb@GA\pb@O\ifdim\pb@GA<\proofcolumns\pb@M\divide\pb@BA
-\proofcolumns\let\pb@MA\pb@PA\else\divide\pb@GA\proofcolumns\let\pb@MA\pb@OA
-\fi\fi\dimen@\lastkern\unkern\setbox\@ne\lastbox\pb@RA\setbox\pb@HA\hbox{\box
-\@ne\kern\dimen@}\advance\pb@U-\wd\pb@HA\unkern\loop\setbox\pb@L\lastbox\pb@T
-\lastkern\unkern\setbox\tw@\lastbox\setbox\thr@@\lastbox\count@\lastpenalty
-\unpenalty\pb@MA\pb@JA\setbox\@ne\vbox{\offinterlineskip\pb@QA\thr@@\vfil
-\pb@QA\tw@}\pb@RA\pb@TA{\box\@ne\box\pb@L}\ifnum\count@>\@ne\pb@SA\pb@U
-\lastkern\unkern\repeat\unhbox\pb@HA}\def\pb@NA{\pb@T\pb@FA\setbox\@ne
-\lastbox\advance\pb@T-\wd\@ne\dimen@\lastkern\unkern\unkern\kern\dimen@\pb@RA
-\box\@ne\advance\pb@T-\dimen@}\def\pb@OA{\ifnum\@ne=\count@\pb@NA\fi}\def
-\pb@PA{\pb@GA\wd\pb@L\advance\pb@GA\pb@BA\pb@OA}\def\pb@QA#1{\setbox#1\hbox to%
-\wd\pb@L{\unhbox#1}\wd#1\z@\box#1\relax}\def\pb@RA{\setbox\@ne\vbox to\pb@EA{%
-\offinterlineskip\vskip-\proofboxseparation\unvbox\@ne\vskip-%
-\proofboxseparation\setbox\z@\null\ht\z@-\pb@DA\dp\z@\pb@DA\box\z@}}\def
-\pb@SA{\setbox\@ne\lastbox\pb@RA\pb@TA{\box\@ne}\ifodd\count@\else\dimen@
-\lastkern\unkern\setbox\@ne\lastbox\pb@RA\pb@TA{\box\@ne\kern\dimen@}\fi}\def
-\pb@TA#1{\setbox\pb@HA\hbox{#1\unhbox\pb@HA}}\let\+\pb@A\proofboxrestoreat
-\endinput\def\x{}%%
-%% \end{document}
-% \fi
diff --git a/Master/texmf-dist/source/latex/proofs/taylor/prooftree-doc.dvi b/Master/texmf-dist/source/latex/proofs/taylor/prooftree-doc.dvi
deleted file mode 100644
index b126e590c26..00000000000
--- a/Master/texmf-dist/source/latex/proofs/taylor/prooftree-doc.dvi
+++ /dev/null
diff --git a/Master/texmf-dist/source/latex/proofs/taylor/prooftree-doc.tex b/Master/texmf-dist/source/latex/proofs/taylor/prooftree-doc.tex
deleted file mode 100644
index a4ed2959b4e..00000000000
--- a/Master/texmf-dist/source/latex/proofs/taylor/prooftree-doc.tex
+++ /dev/null
@@ -1,198 +0,0 @@
-\documentstyle{article}
-\input prooftree
-\title{Build proof tree for Natural Deduction, Sequent Calculus, etc.}
-\author{Paul Taylor\\
-Department of Computing,\\
-Imperial College,\\
-London SW7 2BZ\\
-+44 71 589 5111 {\em ext\/} 5057\\
-{\tt<pt@doc.ic.ac.uk>}}
-\def\X{x}
-\let\imp\Rightarrow
-\def\T{{\rm t\!t}}\def\F{{\rm f\!f}}
-\def\P#1{p#1}%
-\def\Q#1{q#1}%
-\def\E#1#2{\exists#2.\X_{#2}={#1}}
-\def\A#1#2{\exists#1.\left(\left(\E{#1}{#2}\right)\land\Q{#1}\right)}
-\def\B#1#2{\forall#1.\left(\left(\E{#1}{#2}\right)\imp\P{#1}\right)}
-\def\C#1#2{\exists#1.\P{#1}\land\left(\left(\left(\E{#1}{#2}\right)\land\Q{#1}\right)\right)}
-\overfullrule0pt
-\begin{document}
-\maketitle
-Using my Proof Tree macros, you can produce
-{\small
-$$\begin{prooftree}
-\[ \[ [(\A y n)\land(\B w n)]_\alpha
-      \andelim1
-      \A y n
-   \]
-   \kern-26em
-   \[ \[ \[ \[ \[ [(\A y n)\land(\B w n)]_\alpha
-                  \andelim2 \shiftright60pt
-                  \B w n
-               \]
-               \allelim
-               (\E y n)\imp\P y
-            \]
-            \[
-               [(\E y n)\land\Q y]_\beta
-               \andelim1
-               \E y n   
-            \]
-            \impelim \shiftright50pt
-            \P y
-         \]
-         \kern-25pt
-         [(\E y n)\land\Q y]_\beta
-         \andintro
-         \P y\land((\E y n)\land\Q y)
-      \]
-      \existsintro
-      \C z n
-   \]
-   \existselim\beta
-   \C z n
-\]
-\impintro\alpha
-(\A yn)\land(\B w n)\imp(\C z n)
-\end{prooftree}$$}
-using the \TeX\ or \LaTeX\ code
-\begin{verbatim}
-\input prooftree
-$$
-\begin{prooftree}
-\[ \[ [(\A y n)\land(\B w n)]_\alpha
-      \andelim1
-      \A y n
-   \]
-   \kern-26em
-   \[ \[ \[ \[ \[ [(\A y n)\land(\B w n)]_\alpha
-                  \andelim2 \shiftright60pt
-                  \B w n
-               \]
-               \allelim
-               (\E y n)\imp\P y
-            \]
-            \[
-               [(\E y n)\land\Q y]_\beta
-               \andelim1
-               \E y n   
-            \]
-            \impelim \shiftright50pt
-            \P y
-         \]
-         \kern-25pt
-         [(\E y n)\land\Q y]_\beta
-         \andintro
-         \P y\land((\E y n)\land\Q y)
-      \]
-      \existsintro
-      \C z n
-   \]
-   \existselim\beta
-   \C z n
-\]
-\impintro\alpha
-(\A yn)\land(\B w n)\imp(\C z n)
-\end{prooftree}$$
-\end{verbatim}
-
-
-
-In fact the commands \verb/\allintro/, {\it etc.,} are not primitive;
-the basic form is
-\begin{verbatim}
-\[
-	A\quad
-	B
-\justifies
-	A \land B
-\thickness=0.08em
-\shiftright 2em
-\using
-	{\land}{\cal I}
-\]
-\end{verbatim}
-which gives
-$$\begin{prooftree}
-	A\quad
-	B
-\justifies
-	A \land B
-\thickness=0.08em
-\shiftright 2em
-\using
-	{\land}{\cal I}
-\end{prooftree}$$
-The hypotheses may themselves be proof trees (enclosed in
-\verb/\[/\ldots\verb/\]/)
-and the purpose of the macros is to adjust
-the length of the horizontal ``deduction'' line. When the hypotheses
-are proof trees, suitable space is put between them, but of course
-this must be supplied by hand for simple formulae. The \verb/\thickness/
-and \verb/\shiftright/ commands are, of course, optional; they apply to
-the horizontal line and to the positioning of the conclusion relative to
-it. For a double line, use \verb/\Justifies/ instead of \verb/\justifies/.
-
-Notice the overloading of the \verb/\[/\ldots\verb/\]/; the outermost proof
-tree must be enclosed with \verb/\begin{prooftree}/ and \verb/\end{prooftree}/
-or \verb/\prooftree/ and \verb/\endprooftree/.
-
-To get a vertical string of dots instead of the proof rule, do
-\begin{verbatim}
-\[
-	[A]
-\using
-	\pi
-\proofdotseparation=1.2ex
-\proofdotnumber=4
-\leadsto
-	B
-\]
-\end{verbatim}
-to get
-\prooftree
-	[A]
-\using
-	\pi
-\proofdotseparation=1.2ex
-\proofdotnumber=4
-\leadsto
-	B
-\endprooftree
-
-All of of the keywords except \verb/\prooftree/ and \verb/\endprooftree/
-are optional and may appear in any order. They may also be combined in
-\verb/\newcommand/s, for example
-\begin{verbatim}
-\newcommand\Cut{\using\sf cut\thickness.08em\justifies}
-\end{verbatim}
-with the abbreviation
-\begin{verbatim}
-\[ A \vdash B \qquad
-   B \vdash C
-  \Cut
-   A \vdash C
-\]
-\end{verbatim}
-
-\verb/\thickness/ specifies the breadth of the rule in any units, although
-font-relative units such as ex or em are preferable.
-It may optionally be followed by =.
-\verb/\proofrulebreadth=.08em/ or \verb/\setlength\proofrulebreadth{.08em}/
-may also be used either in place of \verb/\thickness/ or globally; the
-default is 0.04em. \verb/\proofdotseparation/ and \verb/\proofdotnumber/
-control the size of the string of dots.
-
-If proof trees and formulae are mixed, some explicit spacing is needed,
-but don't put anything to the left of the left-most (or the right of
-the right-most) hypothesis, or put it in braces, because this will cause
-the indentation to be lost.
-
-By default the conclusion is centered wrt the left-most and right-most
-immediate hypotheses (not their proofs); \verb/\shiftright/ or
-\verb/\shiftleft/ moves it relative to this position.
-(Not sure about this specification or how
-it should affect spreading of proof tree.)
-
-\end{document}
\ No newline at end of file
diff --git a/Master/texmf-dist/source/latex/proofs/taylor/prooftree.tex b/Master/texmf-dist/source/latex/proofs/taylor/prooftree.tex
deleted file mode 100644
index abb7d448642..00000000000
--- a/Master/texmf-dist/source/latex/proofs/taylor/prooftree.tex
+++ /dev/null
@@ -1,347 +0,0 @@
-\message{<Paul Taylor's Proof Trees, 2 August 1996>}
-%% Build proof tree for Natural Deduction, Sequent Calculus, etc.
-%% WITH SHORTENING OF PROOF RULES!
-%% Paul Taylor, begun 10 Oct 1989
-%% *** THIS IS ONLY A PRELIMINARY VERSION AND THINGS MAY CHANGE! ***
-%%
-%% 2 Aug 1996: fixed \mscount and \proofdotnumber
-%%
-%%      \prooftree
-%%              hyp1            produces:
-%%              hyp2
-%%              hyp3            hyp1    hyp2    hyp3
-%%      \justifies              -------------------- rulename
-%%              concl                   concl
-%%      \thickness=0.08em
-%%      \shiftright 2em
-%%      \using
-%%              rulename
-%%      \endprooftree
-%%
-%% where the hypotheses may be similar structures or just formulae.
-%%
-%% To get a vertical string of dots instead of the proof rule, do
-%%
-%%      \prooftree                      which produces:
-%%              [hyp]
-%%      \using                                  [hyp]
-%%              name                              .
-%%      \proofdotseparation=1.2ex                 .name
-%%      \proofdotnumber=4                         .
-%%      \leadsto                                  .
-%%              concl                           concl
-%%      \endprooftree
-%%
-%% Within a prooftree, \[ and \] may be used instead of \prooftree and
-%% \endprooftree; this is not permitted at the outer level because it
-%% conflicts with LaTeX. Also,
-%%      \Justifies
-%% produces a double line. In LaTeX you can use \begin{prooftree} and
-%% \end{prootree} at the outer level (however this will not work for the inner
-%% levels, but in any case why would you want to be so verbose?).
-%%
-%% All of of the keywords except \prooftree and \endprooftree are optional
-%% and may appear in any order. They may also be combined in \newcommand's
-%% eg "\def\Cut{\using\sf cut\thickness.08em\justifies}" with the abbreviation
-%% "\prooftree hyp1 hyp2 \Cut \concl \endprooftree". This is recommended and
-%% some standard abbreviations will be found at the end of this file.
-%%
-%% \thickness specifies the breadth of the rule in any units, although
-%% font-relative units such as "ex" or "em" are preferable.
-%% It may optionally be followed by "=".
-%% \proofrulebreadth=.08em or \setlength\proofrulebreadth{.08em} may also be
-%% used either in place of \thickness or globally; the default is 0.04em.
-%% \proofdotseparation and \proofdotnumber control the size of the
-%% string of dots
-%%
-%% If proof trees and formulae are mixed, some explicit spacing is needed,
-%% but don't put anything to the left of the left-most (or the right of
-%% the right-most) hypothesis, or put it in braces, because this will cause
-%% the indentation to be lost.
-%%
-%% By default the conclusion is centered wrt the left-most and right-most
-%% immediate hypotheses (not their proofs); \shiftright or \shiftleft moves
-%% it relative to this position. (Not sure about this specification or how
-%% it should affect spreading of proof tree.)
-%
-% global assignments to dimensions seem to have the effect of stretching
-% diagrams horizontally.
-%
-%%==========================================================================
-
-\def\introrule{{\cal I}}\def\elimrule{{\cal E}}%%
-\def\andintro{\using{\land}\introrule\justifies}%%
-\def\impelim{\using{\Rightarrow}\elimrule\justifies}%%
-\def\allintro{\using{\forall}\introrule\justifies}%%
-\def\allelim{\using{\forall}\elimrule\justifies}%%
-\def\falseelim{\using{\bot}\elimrule\justifies}%%
-\def\existsintro{\using{\exists}\introrule\justifies}%%
-
-%% #1 is meant to be 1 or 2 for the first or second formula
-\def\andelim#1{\using{\land}#1\elimrule\justifies}%%
-\def\orintro#1{\using{\lor}#1\introrule\justifies}%%
-
-%% #1 is meant to be a label corresponding to the discharged hypothesis/es
-\def\impintro#1{\using{\Rightarrow}\introrule_{#1}\justifies}%%
-\def\orelim#1{\using{\lor}\elimrule_{#1}\justifies}%%
-\def\existselim#1{\using{\exists}\elimrule_{#1}\justifies}
-
-%%==========================================================================
-
-\newdimen\proofrulebreadth \proofrulebreadth=.05em
-\newdimen\proofdotseparation \proofdotseparation=1.25ex
-\newdimen\proofrulebaseline \proofrulebaseline=2ex
-\newcount\proofdotnumber \proofdotnumber=3
-\let\then\relax
-\def\hfi{\hskip0pt plus.0001fil}
-\mathchardef\squigto="3A3B
-%
-% flag where we are
-\newif\ifinsideprooftree\insideprooftreefalse
-\newif\ifonleftofproofrule\onleftofproofrulefalse
-\newif\ifproofdots\proofdotsfalse
-\newif\ifdoubleproof\doubleprooffalse
-\let\wereinproofbit\relax
-%
-% dimensions and boxes of bits
-\newdimen\shortenproofleft
-\newdimen\shortenproofright
-\newdimen\proofbelowshift
-\newbox\proofabove
-\newbox\proofbelow
-\newbox\proofrulename
-%
-% miscellaneous commands for setting values
-\def\shiftproofbelow{\let\next\relax\afterassignment\setshiftproofbelow\dimen0 }
-\def\shiftproofbelowneg{\def\next{\multiply\dimen0 by-1 }%
-\afterassignment\setshiftproofbelow\dimen0 }
-\def\setshiftproofbelow{\next\proofbelowshift=\dimen0 }
-\def\setproofrulebreadth{\proofrulebreadth}
-
-%=============================================================================
-\def\prooftree{% NESTED ZERO (\ifonleftofproofrule)
-%
-% first find out whether we're at the left-hand end of a proof rule
-\ifnum  \lastpenalty=1
-\then   \unpenalty
-\else   \onleftofproofrulefalse
-\fi
-%
-% some space on left (except if we're on left, and no infinity for outermost)
-\ifonleftofproofrule
-\else   \ifinsideprooftree
-        \then   \hskip.5em plus1fil
-        \fi
-\fi
-%
-% begin our proof tree environment
-\bgroup% NESTED ONE (\proofbelow, \proofrulename, \proofabove,
-%               \shortenproofleft, \shortenproofright, \proofrulebreadth)
-\setbox\proofbelow=\hbox{}\setbox\proofrulename=\hbox{}%
-\let\justifies\proofover\let\leadsto\proofoverdots\let\Justifies\proofoverdbl
-\let\using\proofusing\let\[\prooftree
-\ifinsideprooftree\let\]\endprooftree\fi
-\proofdotsfalse\doubleprooffalse
-\let\thickness\setproofrulebreadth
-\let\shiftright\shiftproofbelow \let\shift\shiftproofbelow
-\let\shiftleft\shiftproofbelowneg
-\let\ifwasinsideprooftree\ifinsideprooftree
-\insideprooftreetrue
-%
-% now begin to set the top of the rule (definitions local to it)
-\setbox\proofabove=\hbox\bgroup$\displaystyle % NESTED TWO
-\let\wereinproofbit\prooftree
-%
-% these local variables will be copied out:
-\shortenproofleft=0pt \shortenproofright=0pt \proofbelowshift=0pt
-%
-% flags to enable inner proof tree to detect if on left:
-\onleftofproofruletrue\penalty1
-}
-
-%=============================================================================
-% end whatever box and copy crucial values out of it
-\def\eproofbit{% NESTED TWO
-%
-% various hacks applicable to hypothesis list 
-\ifx    \wereinproofbit\prooftree
-\then   \ifcase \lastpenalty
-        \then   \shortenproofright=0pt  % 0: some other object, no indentation
-        \or     \unpenalty\hfil         % 1: empty hypotheses, just glue
-        \or     \unpenalty\unskip       % 2: just had a tree, remove glue
-        \else   \shortenproofright=0pt  % eh?
-        \fi
-\fi
-%
-% pass out crucial values from scope
-\global\dimen0=\shortenproofleft
-\global\dimen1=\shortenproofright
-\global\dimen2=\proofrulebreadth
-\global\dimen3=\proofbelowshift
-\global\dimen4=\proofdotseparation
-\global\count255=\proofdotnumber
-%
-% end the box
-$\egroup  % NESTED ONE
-%
-% restore the values
-\shortenproofleft=\dimen0
-\shortenproofright=\dimen1
-\proofrulebreadth=\dimen2
-\proofbelowshift=\dimen3
-\proofdotseparation=\dimen4
-\proofdotnumber=\count255
-}
-
-%=============================================================================
-\def\proofover{% NESTED TWO
-\eproofbit % NESTED ONE
-\setbox\proofbelow=\hbox\bgroup % NESTED TWO
-\let\wereinproofbit\proofover
-$\displaystyle
-}%
-%
-%=============================================================================
-\def\proofoverdbl{% NESTED TWO
-\eproofbit % NESTED ONE
-\doubleprooftrue
-\setbox\proofbelow=\hbox\bgroup % NESTED TWO
-\let\wereinproofbit\proofoverdbl
-$\displaystyle
-}%
-%
-%=============================================================================
-\def\proofoverdots{% NESTED TWO
-\eproofbit % NESTED ONE
-\proofdotstrue
-\setbox\proofbelow=\hbox\bgroup % NESTED TWO
-\let\wereinproofbit\proofoverdots
-$\displaystyle
-}%
-%
-%=============================================================================
-\def\proofusing{% NESTED TWO
-\eproofbit % NESTED ONE
-\setbox\proofrulename=\hbox\bgroup % NESTED TWO
-\let\wereinproofbit\proofusing
-\kern0.3em$
-}
-
-%=============================================================================
-\def\endprooftree{% NESTED TWO
-\eproofbit % NESTED ONE
-% \dimen0 =     length of proof rule
-% \dimen1 =     indentation of conclusion wrt rule
-% \dimen2 =     new \shortenproofleft, ie indentation of conclusion
-% \dimen3 =     new \shortenproofright, ie
-%                space on right of conclusion to end of tree
-% \dimen4 =     space on right of conclusion below rule
-  \dimen5 =0pt% spread of hypotheses
-% \dimen6, \dimen7 = height & depth of rule
-%
-% length of rule needed by proof above
-\dimen0=\wd\proofabove \advance\dimen0-\shortenproofleft
-\advance\dimen0-\shortenproofright
-%
-% amount of spare space below
-\dimen1=.5\dimen0 \advance\dimen1-.5\wd\proofbelow
-\dimen4=\dimen1
-\advance\dimen1\proofbelowshift \advance\dimen4-\proofbelowshift
-%
-% conclusion sticks out to left of immediate hypotheses
-\ifdim  \dimen1<0pt
-\then   \advance\shortenproofleft\dimen1
-        \advance\dimen0-\dimen1
-        \dimen1=0pt
-%       now it sticks out to left of tree!
-        \ifdim  \shortenproofleft<0pt
-        \then   \setbox\proofabove=\hbox{%
-                        \kern-\shortenproofleft\unhbox\proofabove}%
-                \shortenproofleft=0pt
-        \fi
-\fi
-%
-% and to the right
-\ifdim  \dimen4<0pt
-\then   \advance\shortenproofright\dimen4
-        \advance\dimen0-\dimen4
-        \dimen4=0pt
-\fi
-%
-% make sure enough space for label
-\ifdim  \shortenproofright<\wd\proofrulename
-\then   \shortenproofright=\wd\proofrulename
-\fi
-%
-% calculate new indentations
-\dimen2=\shortenproofleft \advance\dimen2 by\dimen1
-\dimen3=\shortenproofright\advance\dimen3 by\dimen4
-%
-% make the rule or dots, with name attached
-\ifproofdots
-\then
-        \dimen6=\shortenproofleft \advance\dimen6 .5\dimen0
-        \setbox1=\vbox to\proofdotseparation{\vss\hbox{$\cdot$}\vss}%
-        \setbox0=\hbox{%
-                \advance\dimen6-.5\wd1
-                \kern\dimen6
-                $\vcenter to\proofdotnumber\proofdotseparation
-                        {\leaders\box1\vfill}$%
-                \unhbox\proofrulename}%
-\else   \dimen6=\fontdimen22\the\textfont2 % height of maths axis
-        \dimen7=\dimen6
-        \advance\dimen6by.5\proofrulebreadth
-        \advance\dimen7by-.5\proofrulebreadth
-        \setbox0=\hbox{%
-                \kern\shortenproofleft
-                \ifdoubleproof
-                \then   \hbox to\dimen0{%
-                        $\mathsurround0pt\mathord=\mkern-6mu%
-                        \cleaders\hbox{$\mkern-2mu=\mkern-2mu$}\hfill
-                        \mkern-6mu\mathord=$}%
-                \else   \vrule height\dimen6 depth-\dimen7 width\dimen0
-                \fi
-                \unhbox\proofrulename}%
-        \ht0=\dimen6 \dp0=-\dimen7
-\fi
-%
-% set up to centre outermost tree only
-\let\doll\relax
-\ifwasinsideprooftree
-\then   \let\VBOX\vbox
-\else   \ifmmode\else$\let\doll=$\fi
-        \let\VBOX\vcenter
-\fi
-% this \vbox or \vcenter is the actual output:
-\VBOX   {\baselineskip\proofrulebaseline \lineskip.2ex
-        \expandafter\lineskiplimit\ifproofdots0ex\else-0.6ex\fi
-        \hbox   spread\dimen5   {\hfi\unhbox\proofabove\hfi}%
-        \hbox{\box0}%
-        \hbox   {\kern\dimen2 \box\proofbelow}}\doll%
-%
-% pass new indentations out of scope
-\global\dimen2=\dimen2
-\global\dimen3=\dimen3
-\egroup % NESTED ZERO
-\ifonleftofproofrule
-\then   \shortenproofleft=\dimen2
-\fi
-\shortenproofright=\dimen3
-%
-% some space on right and flag we've just made a tree
-\onleftofproofrulefalse
-\ifinsideprooftree
-\then   \hskip.5em plus 1fil \penalty2
-\fi
-}
-
-%==========================================================================
-% IDEAS
-% 1.    Specification of \shiftright and how to spread trees.
-% 2.    Spacing command \m which causes 1em+1fil spacing, over-riding
-%       exisiting space on sides of trees and not affecting the
-%       detection of being on the left or right.
-% 3.    Hack using \@currenvir to detect LaTeX environment; have to
-%       use \aftergroup to pass \shortenproofleft/right out.
-% 4.    (Pie in the sky) detect how much trees can be "tucked in"
-% 5.    Discharged hypotheses (diagonal lines).