eliminated old copy of proof.sty (1995), prefer the one usually included in current latex distributions (2005);
\usepackage{proof} only where required;
--- a/src/Doc/Classes/document/build Fri Dec 07 17:00:40 2012 +0100
+++ b/src/Doc/Classes/document/build Fri Dec 07 18:05:24 2012 +0100
@@ -10,7 +10,6 @@
cp "$ISABELLE_HOME/src/Doc/iman.sty" .
cp "$ISABELLE_HOME/src/Doc/extra.sty" .
cp "$ISABELLE_HOME/src/Doc/isar.sty" .
-cp "$ISABELLE_HOME/src/Doc/proof.sty" .
cp "$ISABELLE_HOME/src/Doc/manual.bib" .
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Classes/document/root.tex Fri Dec 07 17:00:40 2012 +0100
+++ b/src/Doc/Classes/document/root.tex Fri Dec 07 18:05:24 2012 +0100
@@ -1,6 +1,6 @@
\documentclass[12pt,a4paper,fleqn]{article}
\usepackage{latexsym,graphicx}
-\usepackage{iman,extra,isar,proof}
+\usepackage{iman,extra,isar}
\usepackage{isabelle,isabellesym}
\usepackage{style}
\usepackage{pdfsetup}
--- a/src/Doc/Codegen/document/build Fri Dec 07 17:00:40 2012 +0100
+++ b/src/Doc/Codegen/document/build Fri Dec 07 18:05:24 2012 +0100
@@ -10,7 +10,6 @@
cp "$ISABELLE_HOME/src/Doc/iman.sty" .
cp "$ISABELLE_HOME/src/Doc/extra.sty" .
cp "$ISABELLE_HOME/src/Doc/isar.sty" .
-cp "$ISABELLE_HOME/src/Doc/proof.sty" .
cp "$ISABELLE_HOME/src/Doc/manual.bib" .
for NAME in architecture adapt
--- a/src/Doc/Codegen/document/root.tex Fri Dec 07 17:00:40 2012 +0100
+++ b/src/Doc/Codegen/document/root.tex Fri Dec 07 18:05:24 2012 +0100
@@ -2,7 +2,7 @@
\documentclass[12pt,a4paper,fleqn]{article}
\usepackage{latexsym,graphicx}
\usepackage{multirow}
-\usepackage{iman,extra,isar,proof}
+\usepackage{iman,extra,isar}
\usepackage{isabelle,isabellesym}
\usepackage{style}
\usepackage{pdfsetup}
--- a/src/Doc/HOL/document/build Fri Dec 07 17:00:40 2012 +0100
+++ b/src/Doc/HOL/document/build Fri Dec 07 18:05:24 2012 +0100
@@ -10,7 +10,6 @@
cp "$ISABELLE_HOME/src/Doc/iman.sty" .
cp "$ISABELLE_HOME/src/Doc/extra.sty" .
cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
-cp "$ISABELLE_HOME/src/Doc/proof.sty" .
cp "$ISABELLE_HOME/src/Doc/manual.bib" .
cp "$ISABELLE_HOME/src/Doc/Logics/document/syntax.tex" .
--- a/src/Doc/Intro/document/build Fri Dec 07 17:00:40 2012 +0100
+++ b/src/Doc/Intro/document/build Fri Dec 07 18:05:24 2012 +0100
@@ -10,7 +10,6 @@
cp "$ISABELLE_HOME/src/Doc/iman.sty" .
cp "$ISABELLE_HOME/src/Doc/extra.sty" .
cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
-cp "$ISABELLE_HOME/src/Doc/proof.sty" .
cp "$ISABELLE_HOME/src/Doc/manual.bib" .
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/IsarImplementation/document/build Fri Dec 07 17:00:40 2012 +0100
+++ b/src/Doc/IsarImplementation/document/build Fri Dec 07 18:05:24 2012 +0100
@@ -10,7 +10,6 @@
cp "$ISABELLE_HOME/src/Doc/iman.sty" .
cp "$ISABELLE_HOME/src/Doc/extra.sty" .
cp "$ISABELLE_HOME/src/Doc/isar.sty" .
-cp "$ISABELLE_HOME/src/Doc/proof.sty" .
cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
cp "$ISABELLE_HOME/src/Doc/underscore.sty" .
cp "$ISABELLE_HOME/src/Doc/manual.bib" .
--- a/src/Doc/Logics/document/build Fri Dec 07 17:00:40 2012 +0100
+++ b/src/Doc/Logics/document/build Fri Dec 07 18:05:24 2012 +0100
@@ -10,7 +10,6 @@
cp "$ISABELLE_HOME/src/Doc/iman.sty" .
cp "$ISABELLE_HOME/src/Doc/extra.sty" .
cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
-cp "$ISABELLE_HOME/src/Doc/proof.sty" .
cp "$ISABELLE_HOME/src/Doc/manual.bib" .
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/ROOT Fri Dec 07 17:00:40 2012 +0100
+++ b/src/Doc/ROOT Fri Dec 07 18:05:24 2012 +0100
@@ -8,7 +8,6 @@
"../iman.sty"
"../extra.sty"
"../isar.sty"
- "../proof.sty"
"../manual.bib"
"document/build"
"document/root.tex"
@@ -31,7 +30,6 @@
"../iman.sty"
"../extra.sty"
"../isar.sty"
- "../proof.sty"
"../manual.bib"
"document/adapt.tex"
"document/architecture.tex"
@@ -65,7 +63,6 @@
"../iman.sty"
"../extra.sty"
"../ttbox.sty"
- "../proof.sty"
"../manual.bib"
"document/build"
"document/root.tex"
@@ -89,7 +86,6 @@
"../iman.sty"
"../extra.sty"
"../isar.sty"
- "../proof.sty"
"../ttbox.sty"
"../underscore.sty"
"../manual.bib"
@@ -167,7 +163,6 @@
"../iman.sty"
"../extra.sty"
"../ttbox.sty"
- "../proof.sty"
"../manual.bib"
"document/build"
"document/root.tex"
@@ -181,7 +176,6 @@
"../iman.sty"
"../extra.sty"
"../ttbox.sty"
- "../proof.sty"
"../manual.bib"
"../Logics/document/syntax.tex"
"document/build"
@@ -201,7 +195,6 @@
"../pdfsetup.sty"
"../isar.sty"
"../ttbox.sty"
- "../proof.sty"
"../manual.bib"
"../Logics/document/syntax.tex"
"document/build"
@@ -258,7 +251,6 @@
"../iman.sty"
"../extra.sty"
"../ttbox.sty"
- "../proof.sty"
"../manual.bib"
"document/build"
"document/root.tex"
@@ -363,7 +355,6 @@
"ToyList/ToyList1"
"ToyList/ToyList2"
"../pdfsetup.sty"
- "../proof.sty"
"../ttbox.sty"
"../manual.bib"
"document/advanced0.tex"
--- a/src/Doc/Ref/document/build Fri Dec 07 17:00:40 2012 +0100
+++ b/src/Doc/Ref/document/build Fri Dec 07 18:05:24 2012 +0100
@@ -10,7 +10,6 @@
cp "$ISABELLE_HOME/src/Doc/iman.sty" .
cp "$ISABELLE_HOME/src/Doc/extra.sty" .
cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
-cp "$ISABELLE_HOME/src/Doc/proof.sty" .
cp "$ISABELLE_HOME/src/Doc/manual.bib" .
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Ref/document/root.tex Fri Dec 07 17:00:40 2012 +0100
+++ b/src/Doc/Ref/document/root.tex Fri Dec 07 18:05:24 2012 +0100
@@ -1,5 +1,5 @@
\documentclass[12pt,a4paper]{report}
-\usepackage{graphicx,iman,extra,ttbox,proof,pdfsetup}
+\usepackage{graphicx,iman,extra,ttbox,pdfsetup}
\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Isabelle Reference Manual}
--- a/src/Doc/Tutorial/document/build Fri Dec 07 17:00:40 2012 +0100
+++ b/src/Doc/Tutorial/document/build Fri Dec 07 18:05:24 2012 +0100
@@ -7,7 +7,6 @@
"$ISABELLE_TOOL" logo HOL
-cp "$ISABELLE_HOME/src/Doc/proof.sty" .
cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
cp "$ISABELLE_HOME/src/Doc/manual.bib" .
--- a/src/Doc/ZF/document/build Fri Dec 07 17:00:40 2012 +0100
+++ b/src/Doc/ZF/document/build Fri Dec 07 18:05:24 2012 +0100
@@ -9,7 +9,6 @@
cp "$ISABELLE_HOME/src/Doc/isar.sty" .
cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
-cp "$ISABELLE_HOME/src/Doc/proof.sty" .
cp "$ISABELLE_HOME/src/Doc/manual.bib" .
cp "$ISABELLE_HOME/src/Doc/Logics/document/syntax.tex" .
--- a/src/Doc/proof.sty Fri Dec 07 17:00:40 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,272 +0,0 @@
-\ProvidesPackage{proof}[1995/05/22]
-% proof.sty (Proof Figure Macros)
-%
-% 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
-% 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>.
-%
-% \infer=<Lower><Uppers>
-% draws a double-ruled deduction.
-%
-% \infer=[<Label>]<Lower><Uppers>
-% draws a double-ruled 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@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
-
-\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.
-%TEMPORARILY DELETED BY LCP DUE TO CONFLICT WITH CLASS "amsmath.sty"
-
-\def\@SaveMath{}
-
-\def\@RestoreMath{}
-
-% 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}{\relax
- \@ifnextchar ={\@inferDoubleRule}{\@inferOneStep}}}
-
-\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]}}
-
-% \@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, 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
-%
- \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
- \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
-%
- \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
-}
-\endinput