diff -r 76aa0d5554f0 -r 20251c80be78 doc-src/proof.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/proof.sty	Fri May 02 16:18:11 1997 +0200
@@ -0,0 +1,250 @@
+%	proof.sty	(Proof Figure Macros)
+%
+% 	version 1.0
+%	October 13, 1990
+% 	Copyright (C) 1990 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)
+% 
+% This program is free software; you can redistribute it or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation; either versions 1, or (at your option)
+% any later version.
+% 
+% This program is distributed in the hope that it will be useful
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+% GNU General Public License for more details.
+%
+%	Usage:
+%		In \documentstyle, specify an optional style `proof', say,
+%			\documentstyle[proof]{article}.
+%
+%	The following macros are available:
+%
+%	In all the following macros, all the arguments such as
+%	<Lowers> and <Uppers> are processed in math mode.
+%
+%	\infer<Lower><Uppers>
+%		draws an inference.
+%
+%		Use & in <Uppers> to delimit upper formulae.
+%		<Uppers> consists more than 0 formulae.
+%
+%		\infer returns \hbox{ ... } or \vbox{ ... } and
+%		sets \@LeftOffset and \@RightOffset globally.
+%
+%	\infer[<Label>]<Lower><Uppers>
+%		draws an inference labeled with <Label>.
+%
+%	\infer*<Lower><Uppers>
+%		draws a many step deduction.
+%
+%	\infer*[<Label>]<Lower><Uppers>
+%		draws a many step deduction labeled with <Label>.
+%
+%	\deduce<Lower><Uppers>
+%		draws an inference without a rule.
+%
+%	\deduce[<Proof>]<Lower><Uppers>
+%		draws a many step deduction with a proof name.
+%
+%	Example:
+%		If you want to write
+%       	       	    B C
+%		 	   -----
+%		       A     D
+%		      ----------
+%			  E
+%	use
+%		\infer{E}{
+%			A
+%			&
+%			\infer{D}{B & C}
+%		}
+%
+
+%	Style Parameters
+
+\newdimen\inferLineSkip		\inferLineSkip=2pt
+\newdimen\inferLabelSkip	\inferLabelSkip=5pt
+\def\inferTabSkip{\quad}
+
+%	Variables
+
+\newdimen\@LeftOffset	% global
+\newdimen\@RightOffset	% global
+\newdimen\@SavedLeftOffset	% safe from users
+
+\newdimen\UpperWidth
+\newdimen\LowerWidth
+\newdimen\LowerHeight
+\newdimen\UpperLeftOffset
+\newdimen\UpperRightOffset
+\newdimen\UpperCenter
+\newdimen\LowerCenter
+\newdimen\UpperAdjust
+\newdimen\RuleAdjust
+\newdimen\LowerAdjust
+\newdimen\RuleWidth
+\newdimen\HLabelAdjust
+\newdimen\VLabelAdjust
+\newdimen\WidthAdjust
+
+\newbox\@UpperPart
+\newbox\@LowerPart
+\newbox\@LabelPart
+\newbox\ResultBox
+
+%	Flags
+
+\newif\if@inferRule	% whether \@infer draws a rule.
+\newif\if@ReturnLeftOffset	% whether \@infer returns \@LeftOffset.
+\newif\if@MathSaved	% whether inner math mode where \infer or
+			% \deduce appears.
+
+%	Special Fonts
+
+\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
+    \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
+
+%	Math Save Macros
+%
+%	\@SaveMath is called in the very begining of toplevel macros
+%	which are \infer and \deduce.
+%	\@RestoreMath is called in the very last before toplevel macros end.
+%	Remark \infer and \deduce ends calling \@infer.
+
+\def\@SaveMath{\@MathSavedfalse \ifmmode \ifinner
+	\relax $\relax \@MathSavedtrue \fi\fi }
+
+\def\@RestoreMath{\if@MathSaved \relax $\relax\fi }
+
+%	Macros
+
+\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
+	\ifx \@tempa \@tempb #2\else #3\fi }
+
+\def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\@inferOneStep}}
+
+\def\@inferOneStep{\@inferRuletrue
+	\@ifnextchar [{\@infer}{\@infer[\@empty]}}
+
+\def\@inferSteps*{\@ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
+
+\def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
+
+\def\deduce{\@SaveMath \@ifnextchar [{\@deduce{\@empty}}
+	{\@inferRulefalse \@infer[\@empty]}}
+
+%	\@deduce<Proof Label>[<Proof>]<Lower><Uppers>
+
+\def\@deduce#1[#2]#3#4{\@inferRulefalse
+	\@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
+
+%	\@infer[<Label>]<Lower><Uppers>
+%		If \@inferRuletrue, draws a rule and <Label> is right to
+%		a rule.
+%		Otherwise, draws no rule and <Label> is right to <Lower>.
+
+\def\@infer[#1]#2#3{\relax
+% Get parameters
+	\if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
+	\setbox\@LabelPart=\hbox{$#1$}\relax
+	\setbox\@LowerPart=\hbox{$#2$}\relax
+%
+	\global\@LeftOffset=0pt
+	\setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
+		\global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
+		\inferTabSkip
+		\global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
+		#3\cr}}\relax
+%			Here is a little trick.
+%			\@ReturnLeftOffsettrue(false) influences on \infer or
+%			\deduce placed in ## locally
+%			because of \@SaveMath and \@RestoreMath.
+	\UpperLeftOffset=\@LeftOffset
+	\UpperRightOffset=\@RightOffset
+% Calculate Adjustments
+	\LowerWidth=\wd\@LowerPart
+	\LowerHeight=\ht\@LowerPart
+	\LowerCenter=0.5\LowerWidth
+%
+	\UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
+	\advance\UpperWidth by -\UpperRightOffset
+	\UpperCenter=\UpperLeftOffset
+	\advance\UpperCenter by 0.5\UpperWidth
+%
+	\ifdim \UpperWidth > \LowerWidth
+		% \UpperCenter > \LowerCenter
+	\UpperAdjust=0pt
+	\RuleAdjust=\UpperLeftOffset
+	\LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
+	\RuleWidth=\UpperWidth
+	\global\@LeftOffset=\LowerAdjust
+%
+	\else	% \UpperWidth <= \LowerWidth
+	\ifdim \UpperCenter > \LowerCenter
+%
+	\UpperAdjust=0pt
+	\RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
+	\LowerAdjust=\RuleAdjust
+	\RuleWidth=\LowerWidth
+	\global\@LeftOffset=\LowerAdjust
+%
+	\else	% \UpperWidth <= \LowerWidth
+		% \UpperCenter <= \LowerCenter
+%
+	\UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
+	\RuleAdjust=0pt
+	\LowerAdjust=0pt
+	\RuleWidth=\LowerWidth
+	\global\@LeftOffset=0pt
+%
+	\fi\fi
+% Make a box
+	\if@inferRule
+%
+	\setbox\ResultBox=\vbox{
+		\moveright \UpperAdjust \box\@UpperPart
+		\nointerlineskip \kern\inferLineSkip
+		\moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
+		\nointerlineskip \kern\inferLineSkip
+		\moveright \LowerAdjust \box\@LowerPart }\relax
+%
+	\@ifEmpty{#1}{}{\relax
+%
+	\HLabelAdjust=\wd\ResultBox	\advance\HLabelAdjust by -\RuleAdjust
+	\advance\HLabelAdjust by -\RuleWidth
+	\WidthAdjust=\HLabelAdjust
+	\advance\WidthAdjust by -\inferLabelSkip
+	\advance\WidthAdjust by -\wd\@LabelPart
+	\ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
+%
+	\VLabelAdjust=\dp\@LabelPart
+	\advance\VLabelAdjust by -\ht\@LabelPart
+	\VLabelAdjust=0.5\VLabelAdjust	\advance\VLabelAdjust by \LowerHeight
+	\advance\VLabelAdjust by \inferLineSkip
+%
+	\setbox\ResultBox=\hbox{\box\ResultBox
+		\kern -\HLabelAdjust \kern\inferLabelSkip
+		\raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
+%
+	}\relax % end @ifEmpty
+%
+	\else % \@inferRulefalse
+%
+	\setbox\ResultBox=\vbox{
+		\moveright \UpperAdjust \box\@UpperPart
+		\nointerlineskip \kern\inferLineSkip
+		\moveright \LowerAdjust \hbox{\unhbox\@LowerPart
+			\@ifEmpty{#1}{}{\relax
+			\kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
+	\fi
+%
+	\global\@RightOffset=\wd\ResultBox
+	\global\advance\@RightOffset by -\@LeftOffset
+	\global\advance\@RightOffset by -\LowerWidth
+	\if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
+%
+	\box\ResultBox
+	\@RestoreMath
+}