summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/proofs/taylor/boxproof-old.tex
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/source/latex/proofs/taylor/boxproof-old.tex')
-rw-r--r--Master/texmf-dist/source/latex/proofs/taylor/boxproof-old.tex142
1 files changed, 0 insertions, 142 deletions
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