1.1 --- a/src/Doc/proof.sty Fri Dec 07 17:00:40 2012 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,272 +0,0 @@
1.4 -\ProvidesPackage{proof}[1995/05/22]
1.5 -% proof.sty (Proof Figure Macros)
1.6 -%
1.7 -% version 2.0
1.8 -% June 24, 1991
1.9 -% Copyright (C) 1990,1991 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)
1.10 -%
1.11 -%Modified for LaTeX-2e by L. C. Paulson
1.12 -%
1.13 -% This program is free software; you can redistribute it or modify
1.14 -% it under the terms of the GNU General Public License as published by
1.15 -% the Free Software Foundation; either versions 1, or (at your option)
1.16 -% any later version.
1.17 -%
1.18 -% This program is distributed in the hope that it will be useful
1.19 -% but WITHOUT ANY WARRANTY; without even the implied warranty of
1.20 -% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
1.21 -% GNU General Public License for more details.
1.22 -%
1.23 -% Usage:
1.24 -% In \documentstyle, specify an optional style `proof', say,
1.25 -% \documentstyle[proof]{article}.
1.26 -%
1.27 -% The following macros are available:
1.28 -%
1.29 -% In all the following macros, all the arguments such as
1.30 -% <Lowers> and <Uppers> are processed in math mode.
1.31 -%
1.32 -% \infer<Lower><Uppers>
1.33 -% draws an inference.
1.34 -%
1.35 -% Use & in <Uppers> to delimit upper formulae.
1.36 -% <Uppers> consists more than 0 formulae.
1.37 -%
1.38 -% \infer returns \hbox{ ... } or \vbox{ ... } and
1.39 -% sets \@LeftOffset and \@RightOffset globally.
1.40 -%
1.41 -% \infer[<Label>]<Lower><Uppers>
1.42 -% draws an inference labeled with <Label>.
1.43 -%
1.44 -% \infer*<Lower><Uppers>
1.45 -% draws a many step deduction.
1.46 -%
1.47 -% \infer*[<Label>]<Lower><Uppers>
1.48 -% draws a many step deduction labeled with <Label>.
1.49 -%
1.50 -% \infer=<Lower><Uppers>
1.51 -% draws a double-ruled deduction.
1.52 -%
1.53 -% \infer=[<Label>]<Lower><Uppers>
1.54 -% draws a double-ruled deduction labeled with <Label>.
1.55 -%
1.56 -% \deduce<Lower><Uppers>
1.57 -% draws an inference without a rule.
1.58 -%
1.59 -% \deduce[<Proof>]<Lower><Uppers>
1.60 -% draws a many step deduction with a proof name.
1.61 -%
1.62 -% Example:
1.63 -% If you want to write
1.64 -% B C
1.65 -% -----
1.66 -% A D
1.67 -% ----------
1.68 -% E
1.69 -% use
1.70 -% \infer{E}{
1.71 -% A
1.72 -% &
1.73 -% \infer{D}{B & C}
1.74 -% }
1.75 -%
1.76 -
1.77 -% Style Parameters
1.78 -
1.79 -\newdimen\inferLineSkip \inferLineSkip=2pt
1.80 -\newdimen\inferLabelSkip \inferLabelSkip=5pt
1.81 -\def\inferTabSkip{\quad}
1.82 -
1.83 -% Variables
1.84 -
1.85 -\newdimen\@LeftOffset % global
1.86 -\newdimen\@RightOffset % global
1.87 -\newdimen\@SavedLeftOffset % safe from users
1.88 -
1.89 -\newdimen\UpperWidth
1.90 -\newdimen\LowerWidth
1.91 -\newdimen\LowerHeight
1.92 -\newdimen\UpperLeftOffset
1.93 -\newdimen\UpperRightOffset
1.94 -\newdimen\UpperCenter
1.95 -\newdimen\LowerCenter
1.96 -\newdimen\UpperAdjust
1.97 -\newdimen\RuleAdjust
1.98 -\newdimen\LowerAdjust
1.99 -\newdimen\RuleWidth
1.100 -\newdimen\HLabelAdjust
1.101 -\newdimen\VLabelAdjust
1.102 -\newdimen\WidthAdjust
1.103 -
1.104 -\newbox\@UpperPart
1.105 -\newbox\@LowerPart
1.106 -\newbox\@LabelPart
1.107 -\newbox\ResultBox
1.108 -
1.109 -% Flags
1.110 -
1.111 -\newif\if@inferRule % whether \@infer draws a rule.
1.112 -\newif\if@DoubleRule % whether \@infer draws doulbe rules.
1.113 -\newif\if@ReturnLeftOffset % whether \@infer returns \@LeftOffset.
1.114 -\newif\if@MathSaved % whether inner math mode where \infer or
1.115 - % \deduce appears.
1.116 -
1.117 -% Special Fonts
1.118 -
1.119 -\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
1.120 - \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
1.121 -
1.122 -% Math Save Macros
1.123 -%
1.124 -% \@SaveMath is called in the very begining of toplevel macros
1.125 -% which are \infer and \deduce.
1.126 -% \@RestoreMath is called in the very last before toplevel macros end.
1.127 -% Remark \infer and \deduce ends calling \@infer.
1.128 -%TEMPORARILY DELETED BY LCP DUE TO CONFLICT WITH CLASS "amsmath.sty"
1.129 -
1.130 -\def\@SaveMath{}
1.131 -
1.132 -\def\@RestoreMath{}
1.133 -
1.134 -% Macros
1.135 -
1.136 -\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
1.137 - \ifx \@tempa \@tempb #2\else #3\fi }
1.138 -
1.139 -\def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\relax
1.140 - \@ifnextchar ={\@inferDoubleRule}{\@inferOneStep}}}
1.141 -
1.142 -\def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse
1.143 - \@ifnextchar [{\@infer}{\@infer[\@empty]}}
1.144 -
1.145 -\def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue
1.146 - \@ifnextchar [{\@infer}{\@infer[\@empty]}}
1.147 -
1.148 -\def\@inferSteps*{\@ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
1.149 -
1.150 -\def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
1.151 -
1.152 -\def\deduce{\@SaveMath \@ifnextchar [{\@deduce{\@empty}}
1.153 - {\@inferRulefalse \@infer[\@empty]}}
1.154 -
1.155 -% \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
1.156 -
1.157 -\def\@deduce#1[#2]#3#4{\@inferRulefalse
1.158 - \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
1.159 -
1.160 -% \@infer[<Label>]<Lower><Uppers>
1.161 -% If \@inferRuletrue, it draws a rule and <Label> is right to
1.162 -% a rule. In this case, if \@DoubleRuletrue, it draws
1.163 -% double rules.
1.164 -%
1.165 -% Otherwise, draws no rule and <Label> is right to <Lower>.
1.166 -
1.167 -\def\@infer[#1]#2#3{\relax
1.168 -% Get parameters
1.169 - \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
1.170 - \setbox\@LabelPart=\hbox{$#1$}\relax
1.171 - \setbox\@LowerPart=\hbox{$#2$}\relax
1.172 -%
1.173 - \global\@LeftOffset=0pt
1.174 - \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
1.175 - \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
1.176 - \inferTabSkip
1.177 - \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
1.178 - #3\cr}}\relax
1.179 -% Here is a little trick.
1.180 -% \@ReturnLeftOffsettrue(false) influences on \infer or
1.181 -% \deduce placed in ## locally
1.182 -% because of \@SaveMath and \@RestoreMath.
1.183 - \UpperLeftOffset=\@LeftOffset
1.184 - \UpperRightOffset=\@RightOffset
1.185 -% Calculate Adjustments
1.186 - \LowerWidth=\wd\@LowerPart
1.187 - \LowerHeight=\ht\@LowerPart
1.188 - \LowerCenter=0.5\LowerWidth
1.189 -%
1.190 - \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
1.191 - \advance\UpperWidth by -\UpperRightOffset
1.192 - \UpperCenter=\UpperLeftOffset
1.193 - \advance\UpperCenter by 0.5\UpperWidth
1.194 -%
1.195 - \ifdim \UpperWidth > \LowerWidth
1.196 - % \UpperCenter > \LowerCenter
1.197 - \UpperAdjust=0pt
1.198 - \RuleAdjust=\UpperLeftOffset
1.199 - \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
1.200 - \RuleWidth=\UpperWidth
1.201 - \global\@LeftOffset=\LowerAdjust
1.202 -%
1.203 - \else % \UpperWidth <= \LowerWidth
1.204 - \ifdim \UpperCenter > \LowerCenter
1.205 -%
1.206 - \UpperAdjust=0pt
1.207 - \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
1.208 - \LowerAdjust=\RuleAdjust
1.209 - \RuleWidth=\LowerWidth
1.210 - \global\@LeftOffset=\LowerAdjust
1.211 -%
1.212 - \else % \UpperWidth <= \LowerWidth
1.213 - % \UpperCenter <= \LowerCenter
1.214 -%
1.215 - \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
1.216 - \RuleAdjust=0pt
1.217 - \LowerAdjust=0pt
1.218 - \RuleWidth=\LowerWidth
1.219 - \global\@LeftOffset=0pt
1.220 -%
1.221 - \fi\fi
1.222 -% Make a box
1.223 - \if@inferRule
1.224 -%
1.225 - \setbox\ResultBox=\vbox{
1.226 - \moveright \UpperAdjust \box\@UpperPart
1.227 - \nointerlineskip \kern\inferLineSkip
1.228 - \if@DoubleRule
1.229 - \moveright \RuleAdjust \vbox{\hrule width\RuleWidth
1.230 - \kern 1pt\hrule width\RuleWidth}\relax
1.231 - \else
1.232 - \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
1.233 - \fi
1.234 - \nointerlineskip \kern\inferLineSkip
1.235 - \moveright \LowerAdjust \box\@LowerPart }\relax
1.236 -%
1.237 - \@ifEmpty{#1}{}{\relax
1.238 -%
1.239 - \HLabelAdjust=\wd\ResultBox \advance\HLabelAdjust by -\RuleAdjust
1.240 - \advance\HLabelAdjust by -\RuleWidth
1.241 - \WidthAdjust=\HLabelAdjust
1.242 - \advance\WidthAdjust by -\inferLabelSkip
1.243 - \advance\WidthAdjust by -\wd\@LabelPart
1.244 - \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
1.245 -%
1.246 - \VLabelAdjust=\dp\@LabelPart
1.247 - \advance\VLabelAdjust by -\ht\@LabelPart
1.248 - \VLabelAdjust=0.5\VLabelAdjust \advance\VLabelAdjust by \LowerHeight
1.249 - \advance\VLabelAdjust by \inferLineSkip
1.250 -%
1.251 - \setbox\ResultBox=\hbox{\box\ResultBox
1.252 - \kern -\HLabelAdjust \kern\inferLabelSkip
1.253 - \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
1.254 -%
1.255 - }\relax % end @ifEmpty
1.256 -%
1.257 - \else % \@inferRulefalse
1.258 -%
1.259 - \setbox\ResultBox=\vbox{
1.260 - \moveright \UpperAdjust \box\@UpperPart
1.261 - \nointerlineskip \kern\inferLineSkip
1.262 - \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
1.263 - \@ifEmpty{#1}{}{\relax
1.264 - \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
1.265 - \fi
1.266 -%
1.267 - \global\@RightOffset=\wd\ResultBox
1.268 - \global\advance\@RightOffset by -\@LeftOffset
1.269 - \global\advance\@RightOffset by -\LowerWidth
1.270 - \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
1.271 -%
1.272 - \box\ResultBox
1.273 - \@RestoreMath
1.274 -}
1.275 -\endinput