diff -r 3f0ab2c306f7 -r feb7a5d01c1e doc-src/proof.sty
--- a/doc-src/proof.sty	Wed May 07 13:51:22 1997 +0200
+++ b/doc-src/proof.sty	Wed May 07 16:26:02 1997 +0200
@@ -1,8 +1,11 @@
-%	proof.sty	(Proof Figure Macros)
+\ProvidesPackage{proof}[1995/05/22]
+%       proof.sty       (Proof Figure Macros)
 %
-% 	version 1.0
-%	October 13, 1990
-% 	Copyright (C) 1990 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)
+%       version 2.0
+%       June 24, 1991
+%       Copyright (C) 1990,1991 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)
+%
+%Modified for LaTeX-2e by L. C. Paulson
 % 
 % This program is free software; you can redistribute it or modify
 % it under the terms of the GNU General Public License as published by
@@ -14,65 +17,71 @@
 % 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}.
+%       Usage:
+%               In \documentstyle, specify an optional style `proof', say,
+%                       \documentstyle[proof]{article}.
 %
-%	The following macros are available:
+%       The following macros are available:
 %
-%	In all the following macros, all the arguments such as
-%	<Lowers> and <Uppers> are processed in math mode.
+%       In all the following macros, all the arguments such as
+%       <Lowers> and <Uppers> are processed in math mode.
 %
-%	\infer<Lower><Uppers>
-%		draws an inference.
+%       \infer<Lower><Uppers>
+%               draws an inference.
 %
-%		Use & in <Uppers> to delimit upper formulae.
-%		<Uppers> consists more than 0 formulae.
+%               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 returns \hbox{ ... } or \vbox{ ... } and
+%               sets \@LeftOffset and \@RightOffset globally.
 %
-%	\infer[<Label>]<Lower><Uppers>
-%		draws an inference labeled with <Label>.
+%       \infer[<Label>]<Lower><Uppers>
+%               draws an inference labeled with <Label>.
 %
-%	\infer*<Lower><Uppers>
-%		draws a many step deduction.
+%       \infer*<Lower><Uppers>
+%               draws a many step deduction.
 %
-%	\infer*[<Label>]<Lower><Uppers>
-%		draws a many step deduction labeled with <Label>.
+%       \infer*[<Label>]<Lower><Uppers>
+%               draws a many step deduction labeled with <Label>.
 %
-%	\deduce<Lower><Uppers>
-%		draws an inference without a rule.
+%       \infer=<Lower><Uppers>
+%               draws a double-ruled deduction.
 %
-%	\deduce[<Proof>]<Lower><Uppers>
-%		draws a many step deduction with a proof name.
+%       \infer=[<Label>]<Lower><Uppers>
+%               draws a double-ruled deduction labeled with <Label>.
 %
-%	Example:
-%		If you want to write
-%       	       	    B C
-%		 	   -----
-%		       A     D
-%		      ----------
-%			  E
-%	use
-%		\infer{E}{
-%			A
-%			&
-%			\infer{D}{B & C}
-%		}
+%       \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
+%       Style Parameters
 
-\newdimen\inferLineSkip		\inferLineSkip=2pt
-\newdimen\inferLabelSkip	\inferLabelSkip=5pt
+\newdimen\inferLineSkip         \inferLineSkip=2pt
+\newdimen\inferLabelSkip        \inferLabelSkip=5pt
 \def\inferTabSkip{\quad}
 
-%	Variables
+%       Variables
 
-\newdimen\@LeftOffset	% global
-\newdimen\@RightOffset	% global
-\newdimen\@SavedLeftOffset	% safe from users
+\newdimen\@LeftOffset   % global
+\newdimen\@RightOffset  % global
+\newdimen\@SavedLeftOffset      % safe from users
 
 \newdimen\UpperWidth
 \newdimen\LowerWidth
@@ -94,157 +103,170 @@
 \newbox\@LabelPart
 \newbox\ResultBox
 
-%	Flags
+%       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.
+\newif\if@inferRule     % whether \@infer draws a rule.
+\newif\if@DoubleRule    % whether \@infer draws doulbe rules.
+\newif\if@ReturnLeftOffset      % whether \@infer returns \@LeftOffset.
+\newif\if@MathSaved     % whether inner math mode where \infer or
+                        % \deduce appears.
 
-%	Special Fonts
+%       Special Fonts
 
 \def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
     \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
 
-%	Math Save Macros
+%       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.
+%       \@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.
+%TEMPORARILY DELETED BY LCP DUE TO CONFLICT WITH CLASS "amsmath.sty"
 
-\def\@SaveMath{\@MathSavedfalse \ifmmode \ifinner
-	\relax $\relax \@MathSavedtrue \fi\fi }
+\def\@SaveMath{}
 
-\def\@RestoreMath{\if@MathSaved \relax $\relax\fi }
+\def\@RestoreMath{}
 
-%	Macros
+%       Macros
 
 \def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
-	\ifx \@tempa \@tempb #2\else #3\fi }
+        \ifx \@tempa \@tempb #2\else #3\fi }
 
-\def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\@inferOneStep}}
+\def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\relax
+        \@ifnextchar ={\@inferDoubleRule}{\@inferOneStep}}}
 
-\def\@inferOneStep{\@inferRuletrue
-	\@ifnextchar [{\@infer}{\@infer[\@empty]}}
+\def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse
+        \@ifnextchar [{\@infer}{\@infer[\@empty]}}
+
+\def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue
+        \@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]}}
+        {\@inferRulefalse \@infer[\@empty]}}
 
-%	\@deduce<Proof Label>[<Proof>]<Lower><Uppers>
+%       \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
 
 \def\@deduce#1[#2]#3#4{\@inferRulefalse
-	\@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
+        \@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>.
+%       \@infer[<Label>]<Lower><Uppers>
+%               If \@inferRuletrue, it draws a rule and <Label> is right to
+%               a rule. In this case, if \@DoubleRuletrue, it draws
+%               double rules.
+%
+%               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
+        \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
+        \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
+        \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
+        \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
+        \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
+        \else   % \UpperWidth <= \LowerWidth
+        \ifdim \UpperCenter > \LowerCenter
 %
-	\UpperAdjust=0pt
-	\RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
-	\LowerAdjust=\RuleAdjust
-	\RuleWidth=\LowerWidth
-	\global\@LeftOffset=\LowerAdjust
+        \UpperAdjust=0pt
+        \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
+        \LowerAdjust=\RuleAdjust
+        \RuleWidth=\LowerWidth
+        \global\@LeftOffset=\LowerAdjust
 %
-	\else	% \UpperWidth <= \LowerWidth
-		% \UpperCenter <= \LowerCenter
+        \else   % \UpperWidth <= \LowerWidth
+                % \UpperCenter <= \LowerCenter
 %
-	\UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
-	\RuleAdjust=0pt
-	\LowerAdjust=0pt
-	\RuleWidth=\LowerWidth
-	\global\@LeftOffset=0pt
+        \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
+        \RuleAdjust=0pt
+        \LowerAdjust=0pt
+        \RuleWidth=\LowerWidth
+        \global\@LeftOffset=0pt
 %
-	\fi\fi
+        \fi\fi
 % Make a box
-	\if@inferRule
+        \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
+        \setbox\ResultBox=\vbox{
+                \moveright \UpperAdjust \box\@UpperPart
+                \nointerlineskip \kern\inferLineSkip
+                \if@DoubleRule
+                \moveright \RuleAdjust \vbox{\hrule width\RuleWidth
+                        \kern 1pt\hrule width\RuleWidth}\relax
+                \else
+                \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
+                \fi
+                \nointerlineskip \kern\inferLineSkip
+                \moveright \LowerAdjust \box\@LowerPart }\relax
 %
-	\@ifEmpty{#1}{}{\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
+        \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
+        \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
+        \setbox\ResultBox=\hbox{\box\ResultBox
+                \kern -\HLabelAdjust \kern\inferLabelSkip
+                \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
 %
-	}\relax % end @ifEmpty
+        }\relax % end @ifEmpty
 %
-	\else % \@inferRulefalse
+        \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
+        \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
+        \global\@RightOffset=\wd\ResultBox
+        \global\advance\@RightOffset by -\@LeftOffset
+        \global\advance\@RightOffset by -\LowerWidth
+        \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
 %
-	\box\ResultBox
-	\@RestoreMath
+        \box\ResultBox
+        \@RestoreMath
 }
+\endinput