improved presentation;
authorwenzelm
Mon Oct 11 20:44:23 1999 +0200 (1999-10-11)
changeset 7833f5288e4b95d1
parent 7832 77bac5d84162
child 7834 915be5b9dc6f
improved presentation;
src/HOL/Isar_examples/BasicLogic.thy
src/HOL/Isar_examples/Cantor.thy
src/HOL/Isar_examples/document/proof.sty
src/HOL/Isar_examples/document/style.tex
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Mon Oct 11 20:43:38 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Mon Oct 11 20:44:23 1999 +0200
     1.3 @@ -170,7 +170,7 @@
     1.4   This may be avoided using \isacommand{from} to focus on $\idt{prems}$
     1.5   (i.e.\ the $A \conj B$ assumption) as the current facts, enabling the
     1.6   use of double-dot proofs.  Note that \isacommand{from} already
     1.7 - involves forward-chaining.
     1.8 + does forward-chaining, involving the \name{conjE} rule.
     1.9  *};
    1.10  
    1.11  lemma "A & B --> B & A";
    1.12 @@ -217,7 +217,7 @@
    1.13  qed;
    1.14  
    1.15  text {*
    1.16 - We can still push forward reasoning a bit further, even at the danger
    1.17 + We can still push forward reasoning a bit further, even at the risk
    1.18   of getting ridiculous.  Note that we force the initial proof step to
    1.19   do nothing, by referring to the ``-'' proof method.
    1.20  *};
    1.21 @@ -246,7 +246,7 @@
    1.22   is no single best way to arrange some pieces of formal reasoning, of
    1.23   course.  Depending on the actual applications, the intended audience
    1.24   etc., certain aspects such as rules~/ methods vs.\ facts have to be
    1.25 - emphasised in an appropriate way.  This requires the proof writer to
    1.26 + emphasized in an appropriate way.  This requires the proof writer to
    1.27   develop good taste, and some practice, of course.
    1.28  *};
    1.29  
    1.30 @@ -275,15 +275,58 @@
    1.31  
    1.32  text {*
    1.33   We rephrase some of the basic reasoning examples of
    1.34 - \cite{isabelle-intro}.
    1.35 + \cite{isabelle-intro} (using HOL rather than FOL).
    1.36  *};
    1.37  
    1.38 -subsubsection {* Propositional proof *};
    1.39 +subsubsection {* A propositional proof *};
    1.40 +
    1.41 +text {*
    1.42 + We consider the proposition $P \disj P \impl P$.  The proof below
    1.43 + involves forward-chaining from $P \disj P$, followed by an explicit
    1.44 + case-analysis on the two \emph{identical} cases.
    1.45 +*};
    1.46  
    1.47  lemma "P | P --> P";
    1.48  proof;
    1.49    assume "P | P";
    1.50 -  then; show P;
    1.51 +  thus P;
    1.52 +  proof                    -- {*
    1.53 +    rule \name{disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
    1.54 +  *};
    1.55 +    assume P; show P; .;
    1.56 +  next;
    1.57 +    assume P; show P; .;
    1.58 +  qed;
    1.59 +qed;
    1.60 +
    1.61 +text {*
    1.62 + Case splits are \emph{not} hardwired into the Isar language as a
    1.63 + special feature.  The \isacommand{next} command used to separate the
    1.64 + cases above is just a short form of managing block structure.
    1.65 +
    1.66 + \medskip In general, applying proof methods may split up a goal into
    1.67 + separate ``cases'', i.e.\ new subgoals with individual local
    1.68 + assumptions.  The corresponding proof text typically mimics this by
    1.69 + establishing results in appropriate contexts, separated by blocks.
    1.70 +
    1.71 + In order to avoid too much explicit bracketing, the Isar system
    1.72 + implicitly opens an additional block for any new goal, the
    1.73 + \isacommand{next} statement then closes one block level, opening a
    1.74 + new one.  The resulting behavior is what one might expect from
    1.75 + separating cases, only that it is more flexible.  E.g. an induction
    1.76 + base case (which does not introduce local assumptions) would
    1.77 + \emph{not} require \isacommand{next} to separate the subsequent step
    1.78 + case.
    1.79 +
    1.80 + \medskip In our example the situation is even simpler, since the two
    1.81 + ``cases'' actually coincide.  Consequently the proof may be rephrased
    1.82 + as follows.
    1.83 +*};
    1.84 +
    1.85 +lemma "P | P --> P";
    1.86 +proof;
    1.87 +  assume "P | P";
    1.88 +  thus P;
    1.89    proof;
    1.90      assume P;
    1.91      show P; .;
    1.92 @@ -291,61 +334,90 @@
    1.93    qed;
    1.94  qed;
    1.95  
    1.96 +text {*
    1.97 + Again, the rather vacuous body of the proof may be collapsed.  Thus
    1.98 + the case analysis degenerates into two assumption steps, which
    1.99 + are implicitly performed when concluding the single rule step of the
   1.100 + double-dot proof below.
   1.101 +*};
   1.102 +
   1.103  lemma "P | P --> P";
   1.104  proof;
   1.105    assume "P | P";
   1.106 -  then; show P; ..;
   1.107 +  thus P; ..;
   1.108  qed;
   1.109  
   1.110  
   1.111 -subsubsection {* Quantifier proof *};
   1.112 +subsubsection {* A quantifier proof *};
   1.113 +
   1.114 +text {*
   1.115 + To illustrate quantifier reasoning, let us prove $(\ex x P \ap (f \ap
   1.116 + x)) \impl (\ex x P \ap x)$.  Informally, this holds because any $a$
   1.117 + with $P \ap (f \ap a)$ may be taken as a witness for the second
   1.118 + existential statement.
   1.119  
   1.120 -lemma "(EX x. P(f(x))) --> (EX x. P(x))";
   1.121 + The first proof is rather verbose, exhibiting quite a lot of
   1.122 + (redundant) detail.  It gives explicit rules, even with some
   1.123 + instantiation.  Furthermore, we encounter two new language elements:
   1.124 + the \isacommand{fix} command augments the context by some new
   1.125 + ``arbitrary, but fixed'' element; the \isacommand{is} annotation
   1.126 + binds term abbreviations by higher-order pattern matching.
   1.127 +*};
   1.128 +
   1.129 +lemma "(EX x. P (f x)) --> (EX x. P x)";
   1.130  proof;
   1.131 -  assume "EX x. P(f(x))";
   1.132 -  then; show "EX x. P(x)";
   1.133 -  proof (rule exE);
   1.134 +  assume "EX x. P (f x)";
   1.135 +  thus "EX x. P x";
   1.136 +  proof (rule exE)             -- {*
   1.137 +    rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
   1.138 +  *};
   1.139      fix a;
   1.140 -    assume "P(f(a))" (is "P(?witness)");
   1.141 +    assume "P (f a)" (is "P ?witness");
   1.142      show ?thesis; by (rule exI [of P ?witness]);
   1.143    qed;
   1.144  qed;
   1.145  
   1.146 -lemma "(EX x. P(f(x))) --> (EX x. P(x))";
   1.147 +text {*
   1.148 + While explicit rule instantiation may occasionally help to improve
   1.149 + the readability of certain aspects of reasoning it is usually quite
   1.150 + redundant.  Above, the basic proof outline gives already enough
   1.151 + structural clues for the system to infer both the rules and their
   1.152 + instances (by higher-order unification).  Thus we may as well prune
   1.153 + the text as follows.
   1.154 +*};
   1.155 +
   1.156 +lemma "(EX x. P (f x)) --> (EX x. P x)";
   1.157  proof;
   1.158 -  assume "EX x. P(f(x))";
   1.159 -  then; show "EX x. P(x)";
   1.160 +  assume "EX x. P (f x)";
   1.161 +  thus "EX x. P x";
   1.162    proof;
   1.163      fix a;
   1.164 -    assume "P(f(a))";
   1.165 +    assume "P (f a)";
   1.166      show ?thesis; ..;
   1.167    qed;
   1.168  qed;
   1.169  
   1.170 -lemma "(EX x. P(f(x))) --> (EX x. P(x))";
   1.171 -  by blast;
   1.172 -
   1.173  
   1.174  subsubsection {* Deriving rules in Isabelle *};
   1.175  
   1.176 -text {* We derive the conjunction elimination rule from the
   1.177 - projections.  The proof below follows the basic reasoning of the
   1.178 - script given in the Isabelle Intro Manual closely.  Although, the
   1.179 - actual underlying operations on rules and proof states are quite
   1.180 - different: Isabelle/Isar supports non-atomic goals and assumptions
   1.181 - fully transparently, while the original Isabelle classic script
   1.182 - depends on the primitive goal command to decompose the rule into
   1.183 - premises and conclusion, with the result emerging by discharging the
   1.184 - context again later. *};
   1.185 +text {*
   1.186 + We derive the conjunction elimination rule from the projections.  The
   1.187 + proof below follows is quite straight-forward, since Isabelle/Isar
   1.188 + supports non-atomic goals and assumptions fully transparently.  Note
   1.189 + that this is in contrast to classic Isabelle: the corresponding
   1.190 + tactic script given in \cite{isabelle-intro} depends on the primitive
   1.191 + goal command to decompose the rule into premises and conclusion, with
   1.192 + the result emerging by discharging the context again later.
   1.193 +*};
   1.194  
   1.195  theorem conjE: "A & B ==> (A ==> B ==> C) ==> C";
   1.196  proof -;
   1.197 -  assume ab: "A & B";
   1.198 +  assume "A & B";
   1.199    assume ab_c: "A ==> B ==> C";
   1.200    show C;
   1.201    proof (rule ab_c);
   1.202 -    from ab; show A; ..;
   1.203 -    from ab; show B; ..;
   1.204 +    show A; by (rule conjunct1);
   1.205 +    show B; by (rule conjunct2);
   1.206    qed;
   1.207  qed;
   1.208  
     2.1 --- a/src/HOL/Isar_examples/Cantor.thy	Mon Oct 11 20:43:38 1999 +0200
     2.2 +++ b/src/HOL/Isar_examples/Cantor.thy	Mon Oct 11 20:44:23 1999 +0200
     2.3 @@ -5,11 +5,8 @@
     2.4  
     2.5  header {* Cantor's Theorem *};
     2.6  
     2.7 -theory Cantor = Main:;
     2.8 -
     2.9 -text {*
    2.10 - This is an Isar'ized version of the final example of the Isabelle/HOL
    2.11 - manual \cite{isabelle-HOL}.
    2.12 +theory Cantor = Main:;verbatim {* \footnote{This is an Isar version of
    2.13 + the final example of the Isabelle/HOL manual \cite{isabelle-HOL}.}
    2.14  *};
    2.15  
    2.16  text {*
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Isar_examples/document/proof.sty	Mon Oct 11 20:44:23 1999 +0200
     3.3 @@ -0,0 +1,254 @@
     3.4 +%       proof.sty       (Proof Figure Macros)
     3.5 +%
     3.6 +%       version 1.0
     3.7 +%       October 13, 1990
     3.8 +%       Copyright (C) 1990 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)
     3.9 +%
    3.10 +% This program is free software; you can redistribute it or modify
    3.11 +% it under the terms of the GNU General Public License as published by
    3.12 +% the Free Software Foundation; either versions 1, or (at your option)
    3.13 +% any later version.
    3.14 +%
    3.15 +% This program is distributed in the hope that it will be useful
    3.16 +% but WITHOUT ANY WARRANTY; without even the implied warranty of
    3.17 +% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    3.18 +% GNU General Public License for more details.
    3.19 +%
    3.20 +%       Usage:
    3.21 +%               In \documentstyle, specify an optional style `proof', say,
    3.22 +%                       \documentstyle[proof]{article}.
    3.23 +%
    3.24 +%       The following macros are available:
    3.25 +%
    3.26 +%       In all the following macros, all the arguments such as
    3.27 +%       <Lowers> and <Uppers> are processed in math mode.
    3.28 +%
    3.29 +%       \infer<Lower><Uppers>
    3.30 +%               draws an inference.
    3.31 +%
    3.32 +%               Use & in <Uppers> to delimit upper formulae.
    3.33 +%               <Uppers> consists more than 0 formulae.
    3.34 +%
    3.35 +%               \infer returns \hbox{ ... } or \vbox{ ... } and
    3.36 +%               sets \@LeftOffset and \@RightOffset globally.
    3.37 +%
    3.38 +%       \infer[<Label>]<Lower><Uppers>
    3.39 +%               draws an inference labeled with <Label>.
    3.40 +%
    3.41 +%       \infer*<Lower><Uppers>
    3.42 +%               draws a many step deduction.
    3.43 +%
    3.44 +%       \infer*[<Label>]<Lower><Uppers>
    3.45 +%               draws a many step deduction labeled with <Label>.
    3.46 +%
    3.47 +%       \deduce<Lower><Uppers>
    3.48 +%               draws an inference without a rule.
    3.49 +%
    3.50 +%       \deduce[<Proof>]<Lower><Uppers>
    3.51 +%               draws a many step deduction with a proof name.
    3.52 +%
    3.53 +%       Example:
    3.54 +%               If you want to write
    3.55 +%                           B C
    3.56 +%                          -----
    3.57 +%                      A     D
    3.58 +%                     ----------
    3.59 +%                         E
    3.60 +%       use
    3.61 +%               \infer{E}{
    3.62 +%                       A
    3.63 +%                       &
    3.64 +%                       \infer{D}{B & C}
    3.65 +%               }
    3.66 +%
    3.67 +
    3.68 +%       Style Parameters
    3.69 +
    3.70 +\newdimen\inferLineSkip         \inferLineSkip=2pt
    3.71 +\newdimen\inferLabelSkip        \inferLabelSkip=5pt
    3.72 +\def\inferTabSkip{\quad}
    3.73 +
    3.74 +%       Variables
    3.75 +
    3.76 +\newdimen\@LeftOffset   % global
    3.77 +\newdimen\@RightOffset  % global
    3.78 +\newdimen\@SavedLeftOffset      % safe from users
    3.79 +
    3.80 +\newdimen\UpperWidth
    3.81 +\newdimen\LowerWidth
    3.82 +\newdimen\LowerHeight
    3.83 +\newdimen\UpperLeftOffset
    3.84 +\newdimen\UpperRightOffset
    3.85 +\newdimen\UpperCenter
    3.86 +\newdimen\LowerCenter
    3.87 +\newdimen\UpperAdjust
    3.88 +\newdimen\RuleAdjust
    3.89 +\newdimen\LowerAdjust
    3.90 +\newdimen\RuleWidth
    3.91 +\newdimen\HLabelAdjust
    3.92 +\newdimen\VLabelAdjust
    3.93 +\newdimen\WidthAdjust
    3.94 +
    3.95 +\newbox\@UpperPart
    3.96 +\newbox\@LowerPart
    3.97 +\newbox\@LabelPart
    3.98 +\newbox\ResultBox
    3.99 +
   3.100 +%       Flags
   3.101 +
   3.102 +\newif\if@inferRule     % whether \@infer draws a rule.
   3.103 +\newif\if@ReturnLeftOffset      % whether \@infer returns \@LeftOffset.
   3.104 +\newif\if@MathSaved     % whether inner math mode where \infer or
   3.105 +                        % \deduce appears.
   3.106 +
   3.107 +%       Special Fonts
   3.108 +
   3.109 +\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
   3.110 +    \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
   3.111 +
   3.112 +%       Math Save Macros
   3.113 +%
   3.114 +%       \@SaveMath is called in the very begining of toplevel macros
   3.115 +%       which are \infer and \deduce.
   3.116 +%       \@RestoreMath is called in the very last before toplevel macros end.
   3.117 +%       Remark \infer and \deduce ends calling \@infer.
   3.118 +
   3.119 +%\def\@SaveMath{\@MathSavedfalse \ifmmode \ifinner
   3.120 +%        \relax $\relax \@MathSavedtrue \fi\fi }
   3.121 +%
   3.122 +%\def\@RestoreMath{\if@MathSaved \relax $\relax\fi }
   3.123 +
   3.124 +\def\@SaveMath{\relax}
   3.125 +\def\@RestoreMath{\relax}
   3.126 +
   3.127 +
   3.128 +%       Macros
   3.129 +
   3.130 +\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
   3.131 +        \ifx \@tempa \@tempb #2\else #3\fi }
   3.132 +
   3.133 +\def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\@inferOneStep}}
   3.134 +
   3.135 +\def\@inferOneStep{\@inferRuletrue
   3.136 +        \@ifnextchar [{\@infer}{\@infer[\@empty]}}
   3.137 +
   3.138 +\def\@inferSteps*{\@ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
   3.139 +
   3.140 +\def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
   3.141 +
   3.142 +\def\deduce{\@SaveMath \@ifnextchar [{\@deduce{\@empty}}
   3.143 +        {\@inferRulefalse \@infer[\@empty]}}
   3.144 +
   3.145 +%       \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
   3.146 +
   3.147 +\def\@deduce#1[#2]#3#4{\@inferRulefalse
   3.148 +        \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
   3.149 +
   3.150 +%       \@infer[<Label>]<Lower><Uppers>
   3.151 +%               If \@inferRuletrue, draws a rule and <Label> is right to
   3.152 +%               a rule.
   3.153 +%               Otherwise, draws no rule and <Label> is right to <Lower>.
   3.154 +
   3.155 +\def\@infer[#1]#2#3{\relax
   3.156 +% Get parameters
   3.157 +        \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
   3.158 +        \setbox\@LabelPart=\hbox{$#1$}\relax
   3.159 +        \setbox\@LowerPart=\hbox{$#2$}\relax
   3.160 +%
   3.161 +        \global\@LeftOffset=0pt
   3.162 +        \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
   3.163 +                \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
   3.164 +                \inferTabSkip
   3.165 +                \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
   3.166 +                #3\cr}}\relax
   3.167 +%                       Here is a little trick.
   3.168 +%                       \@ReturnLeftOffsettrue(false) influences on \infer or
   3.169 +%                       \deduce placed in ## locally
   3.170 +%                       because of \@SaveMath and \@RestoreMath.
   3.171 +        \UpperLeftOffset=\@LeftOffset
   3.172 +        \UpperRightOffset=\@RightOffset
   3.173 +% Calculate Adjustments
   3.174 +        \LowerWidth=\wd\@LowerPart
   3.175 +        \LowerHeight=\ht\@LowerPart
   3.176 +        \LowerCenter=0.5\LowerWidth
   3.177 +%
   3.178 +        \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
   3.179 +        \advance\UpperWidth by -\UpperRightOffset
   3.180 +        \UpperCenter=\UpperLeftOffset
   3.181 +        \advance\UpperCenter by 0.5\UpperWidth
   3.182 +%
   3.183 +        \ifdim \UpperWidth > \LowerWidth
   3.184 +                % \UpperCenter > \LowerCenter
   3.185 +        \UpperAdjust=0pt
   3.186 +        \RuleAdjust=\UpperLeftOffset
   3.187 +        \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
   3.188 +        \RuleWidth=\UpperWidth
   3.189 +        \global\@LeftOffset=\LowerAdjust
   3.190 +%
   3.191 +        \else   % \UpperWidth <= \LowerWidth
   3.192 +        \ifdim \UpperCenter > \LowerCenter
   3.193 +%
   3.194 +        \UpperAdjust=0pt
   3.195 +        \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
   3.196 +        \LowerAdjust=\RuleAdjust
   3.197 +        \RuleWidth=\LowerWidth
   3.198 +        \global\@LeftOffset=\LowerAdjust
   3.199 +%
   3.200 +        \else   % \UpperWidth <= \LowerWidth
   3.201 +                % \UpperCenter <= \LowerCenter
   3.202 +%
   3.203 +        \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
   3.204 +        \RuleAdjust=0pt
   3.205 +        \LowerAdjust=0pt
   3.206 +        \RuleWidth=\LowerWidth
   3.207 +        \global\@LeftOffset=0pt
   3.208 +%
   3.209 +        \fi\fi
   3.210 +% Make a box
   3.211 +        \if@inferRule
   3.212 +%
   3.213 +        \setbox\ResultBox=\vbox{
   3.214 +                \moveright \UpperAdjust \box\@UpperPart
   3.215 +                \nointerlineskip \kern\inferLineSkip
   3.216 +                \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
   3.217 +                \nointerlineskip \kern\inferLineSkip
   3.218 +                \moveright \LowerAdjust \box\@LowerPart }\relax
   3.219 +%
   3.220 +        \@ifEmpty{#1}{}{\relax
   3.221 +%
   3.222 +        \HLabelAdjust=\wd\ResultBox     \advance\HLabelAdjust by -\RuleAdjust
   3.223 +        \advance\HLabelAdjust by -\RuleWidth
   3.224 +        \WidthAdjust=\HLabelAdjust
   3.225 +        \advance\WidthAdjust by -\inferLabelSkip
   3.226 +        \advance\WidthAdjust by -\wd\@LabelPart
   3.227 +        \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
   3.228 +%
   3.229 +        \VLabelAdjust=\dp\@LabelPart
   3.230 +        \advance\VLabelAdjust by -\ht\@LabelPart
   3.231 +        \VLabelAdjust=0.5\VLabelAdjust  \advance\VLabelAdjust by \LowerHeight
   3.232 +        \advance\VLabelAdjust by \inferLineSkip
   3.233 +%
   3.234 +        \setbox\ResultBox=\hbox{\box\ResultBox
   3.235 +                \kern -\HLabelAdjust \kern\inferLabelSkip
   3.236 +                \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
   3.237 +%
   3.238 +        }\relax % end @ifEmpty
   3.239 +%
   3.240 +        \else % \@inferRulefalse
   3.241 +%
   3.242 +        \setbox\ResultBox=\vbox{
   3.243 +                \moveright \UpperAdjust \box\@UpperPart
   3.244 +                \nointerlineskip \kern\inferLineSkip
   3.245 +                \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
   3.246 +                        \@ifEmpty{#1}{}{\relax
   3.247 +                        \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
   3.248 +        \fi
   3.249 +%
   3.250 +        \global\@RightOffset=\wd\ResultBox
   3.251 +        \global\advance\@RightOffset by -\@LeftOffset
   3.252 +        \global\advance\@RightOffset by -\LowerWidth
   3.253 +        \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
   3.254 +%
   3.255 +        \box\ResultBox
   3.256 +        \@RestoreMath
   3.257 +}
     4.1 --- a/src/HOL/Isar_examples/document/style.tex	Mon Oct 11 20:43:38 1999 +0200
     4.2 +++ b/src/HOL/Isar_examples/document/style.tex	Mon Oct 11 20:44:23 1999 +0200
     4.3 @@ -2,12 +2,12 @@
     4.4  %% $Id$
     4.5  
     4.6  \documentclass[11pt,a4paper]{article}
     4.7 -\usepackage{comment,isabelle,pdfsetup}
     4.8 +\usepackage{comment,proof,isabelle,pdfsetup}
     4.9  
    4.10  \renewcommand{\isamarkupheader}[1]{\section{#1}}
    4.11  \parindent 0pt \parskip 0.5ex
    4.12  
    4.13 -\newcommand{\name}[1]{\textsf{#1}}
    4.14 +\newcommand{\name}[1]{\textsl{#1}}
    4.15  
    4.16  \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
    4.17  \newcommand{\var}[1]{{?\!#1}}
    4.18 @@ -22,6 +22,7 @@
    4.19  \newcommand{\ex}[1]{\exists #1\dt\;}
    4.20  \newcommand{\impl}{\rightarrow}
    4.21  \newcommand{\conj}{\land}
    4.22 +\newcommand{\disj}{\lor}
    4.23  
    4.24  
    4.25  %%% Local Variables: