*** empty log message ***
authornipkow
Mon Nov 27 16:40:56 2000 +0100 (2000-11-27)
changeset 10524270b285d48ee
parent 10523 68105cf615fa
child 10525 3e21ab3e5114
*** empty log message ***
doc-src/TutorialI/CTL/PDL.thy
doc-src/TutorialI/CTL/document/PDL.tex
doc-src/TutorialI/proof.sty
doc-src/TutorialI/tutorial.tex
     1.1 --- a/doc-src/TutorialI/CTL/PDL.thy	Mon Nov 27 11:06:28 2000 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/PDL.thy	Mon Nov 27 16:40:56 2000 +0100
     1.3 @@ -96,7 +96,7 @@
     1.4  
     1.5  apply(rule equalityI);
     1.6   apply(rule subsetI);
     1.7 - apply(simp)
     1.8 + apply(simp)(*<*)apply(rename_tac s)(*>*)
     1.9  
    1.10  txt{*\noindent
    1.11  Simplification leaves us with the following first subgoal
     2.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex	Mon Nov 27 11:06:28 2000 +0100
     2.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex	Mon Nov 27 16:40:56 2000 +0100
     2.3 @@ -98,7 +98,7 @@
     2.4  \noindent
     2.5  Simplification leaves us with the following first subgoal
     2.6  \begin{isabelle}%
     2.7 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A%
     2.8 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A%
     2.9  \end{isabelle}
    2.10  which is proved by \isa{lfp}-induction:%
    2.11  \end{isamarkuptxt}%
     3.1 --- a/doc-src/TutorialI/proof.sty	Mon Nov 27 11:06:28 2000 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,272 +0,0 @@
     3.4 -\ProvidesPackage{proof}[1995/05/22]
     3.5 -%       proof.sty       (Proof Figure Macros)
     3.6 -%
     3.7 -%       version 2.0
     3.8 -%       June 24, 1991
     3.9 -%       Copyright (C) 1990,1991 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)
    3.10 -%
    3.11 -%Modified for LaTeX-2e by L. C. Paulson
    3.12 -% 
    3.13 -% This program is free software; you can redistribute it or modify
    3.14 -% it under the terms of the GNU General Public License as published by
    3.15 -% the Free Software Foundation; either versions 1, or (at your option)
    3.16 -% any later version.
    3.17 -% 
    3.18 -% This program is distributed in the hope that it will be useful
    3.19 -% but WITHOUT ANY WARRANTY; without even the implied warranty of
    3.20 -% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    3.21 -% GNU General Public License for more details.
    3.22 -%
    3.23 -%       Usage:
    3.24 -%               In \documentstyle, specify an optional style `proof', say,
    3.25 -%                       \documentstyle[proof]{article}.
    3.26 -%
    3.27 -%       The following macros are available:
    3.28 -%
    3.29 -%       In all the following macros, all the arguments such as
    3.30 -%       <Lowers> and <Uppers> are processed in math mode.
    3.31 -%
    3.32 -%       \infer<Lower><Uppers>
    3.33 -%               draws an inference.
    3.34 -%
    3.35 -%               Use & in <Uppers> to delimit upper formulae.
    3.36 -%               <Uppers> consists more than 0 formulae.
    3.37 -%
    3.38 -%               \infer returns \hbox{ ... } or \vbox{ ... } and
    3.39 -%               sets \@LeftOffset and \@RightOffset globally.
    3.40 -%
    3.41 -%       \infer[<Label>]<Lower><Uppers>
    3.42 -%               draws an inference labeled with <Label>.
    3.43 -%
    3.44 -%       \infer*<Lower><Uppers>
    3.45 -%               draws a many step deduction.
    3.46 -%
    3.47 -%       \infer*[<Label>]<Lower><Uppers>
    3.48 -%               draws a many step deduction labeled with <Label>.
    3.49 -%
    3.50 -%       \infer=<Lower><Uppers>
    3.51 -%               draws a double-ruled deduction.
    3.52 -%
    3.53 -%       \infer=[<Label>]<Lower><Uppers>
    3.54 -%               draws a double-ruled deduction labeled with <Label>.
    3.55 -%
    3.56 -%       \deduce<Lower><Uppers>
    3.57 -%               draws an inference without a rule.
    3.58 -%
    3.59 -%       \deduce[<Proof>]<Lower><Uppers>
    3.60 -%               draws a many step deduction with a proof name.
    3.61 -%
    3.62 -%       Example:
    3.63 -%               If you want to write
    3.64 -%                           B C
    3.65 -%                          -----
    3.66 -%                      A     D
    3.67 -%                     ----------
    3.68 -%                         E
    3.69 -%       use
    3.70 -%               \infer{E}{
    3.71 -%                       A
    3.72 -%                       &
    3.73 -%                       \infer{D}{B & C}
    3.74 -%               }
    3.75 -%
    3.76 -
    3.77 -%       Style Parameters
    3.78 -
    3.79 -\newdimen\inferLineSkip         \inferLineSkip=2pt
    3.80 -\newdimen\inferLabelSkip        \inferLabelSkip=5pt
    3.81 -\def\inferTabSkip{\quad}
    3.82 -
    3.83 -%       Variables
    3.84 -
    3.85 -\newdimen\@LeftOffset   % global
    3.86 -\newdimen\@RightOffset  % global
    3.87 -\newdimen\@SavedLeftOffset      % safe from users
    3.88 -
    3.89 -\newdimen\UpperWidth
    3.90 -\newdimen\LowerWidth
    3.91 -\newdimen\LowerHeight
    3.92 -\newdimen\UpperLeftOffset
    3.93 -\newdimen\UpperRightOffset
    3.94 -\newdimen\UpperCenter
    3.95 -\newdimen\LowerCenter
    3.96 -\newdimen\UpperAdjust
    3.97 -\newdimen\RuleAdjust
    3.98 -\newdimen\LowerAdjust
    3.99 -\newdimen\RuleWidth
   3.100 -\newdimen\HLabelAdjust
   3.101 -\newdimen\VLabelAdjust
   3.102 -\newdimen\WidthAdjust
   3.103 -
   3.104 -\newbox\@UpperPart
   3.105 -\newbox\@LowerPart
   3.106 -\newbox\@LabelPart
   3.107 -\newbox\ResultBox
   3.108 -
   3.109 -%       Flags
   3.110 -
   3.111 -\newif\if@inferRule     % whether \@infer draws a rule.
   3.112 -\newif\if@DoubleRule    % whether \@infer draws doulbe rules.
   3.113 -\newif\if@ReturnLeftOffset      % whether \@infer returns \@LeftOffset.
   3.114 -\newif\if@MathSaved     % whether inner math mode where \infer or
   3.115 -                        % \deduce appears.
   3.116 -
   3.117 -%       Special Fonts
   3.118 -
   3.119 -\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
   3.120 -    \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
   3.121 -
   3.122 -%       Math Save Macros
   3.123 -%
   3.124 -%       \@SaveMath is called in the very begining of toplevel macros
   3.125 -%       which are \infer and \deduce.
   3.126 -%       \@RestoreMath is called in the very last before toplevel macros end.
   3.127 -%       Remark \infer and \deduce ends calling \@infer.
   3.128 -%TEMPORARILY DELETED BY LCP DUE TO CONFLICT WITH CLASS "amsmath.sty"
   3.129 -
   3.130 -\def\@SaveMath{}
   3.131 -
   3.132 -\def\@RestoreMath{}
   3.133 -
   3.134 -%       Macros
   3.135 -
   3.136 -\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
   3.137 -        \ifx \@tempa \@tempb #2\else #3\fi }
   3.138 -
   3.139 -\def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\relax
   3.140 -        \@ifnextchar ={\@inferDoubleRule}{\@inferOneStep}}}
   3.141 -
   3.142 -\def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse
   3.143 -        \@ifnextchar [{\@infer}{\@infer[\@empty]}}
   3.144 -
   3.145 -\def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue
   3.146 -        \@ifnextchar [{\@infer}{\@infer[\@empty]}}
   3.147 -
   3.148 -\def\@inferSteps*{\@ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
   3.149 -
   3.150 -\def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
   3.151 -
   3.152 -\def\deduce{\@SaveMath \@ifnextchar [{\@deduce{\@empty}}
   3.153 -        {\@inferRulefalse \@infer[\@empty]}}
   3.154 -
   3.155 -%       \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
   3.156 -
   3.157 -\def\@deduce#1[#2]#3#4{\@inferRulefalse
   3.158 -        \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
   3.159 -
   3.160 -%       \@infer[<Label>]<Lower><Uppers>
   3.161 -%               If \@inferRuletrue, it draws a rule and <Label> is right to
   3.162 -%               a rule. In this case, if \@DoubleRuletrue, it draws
   3.163 -%               double rules.
   3.164 -%
   3.165 -%               Otherwise, draws no rule and <Label> is right to <Lower>.
   3.166 -
   3.167 -\def\@infer[#1]#2#3{\relax
   3.168 -% Get parameters
   3.169 -        \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
   3.170 -        \setbox\@LabelPart=\hbox{$#1$}\relax
   3.171 -        \setbox\@LowerPart=\hbox{$#2$}\relax
   3.172 -%
   3.173 -        \global\@LeftOffset=0pt
   3.174 -        \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
   3.175 -                \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
   3.176 -                \inferTabSkip
   3.177 -                \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
   3.178 -                #3\cr}}\relax
   3.179 -%                       Here is a little trick.
   3.180 -%                       \@ReturnLeftOffsettrue(false) influences on \infer or
   3.181 -%                       \deduce placed in ## locally
   3.182 -%                       because of \@SaveMath and \@RestoreMath.
   3.183 -        \UpperLeftOffset=\@LeftOffset
   3.184 -        \UpperRightOffset=\@RightOffset
   3.185 -% Calculate Adjustments
   3.186 -        \LowerWidth=\wd\@LowerPart
   3.187 -        \LowerHeight=\ht\@LowerPart
   3.188 -        \LowerCenter=0.5\LowerWidth
   3.189 -%
   3.190 -        \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
   3.191 -        \advance\UpperWidth by -\UpperRightOffset
   3.192 -        \UpperCenter=\UpperLeftOffset
   3.193 -        \advance\UpperCenter by 0.5\UpperWidth
   3.194 -%
   3.195 -        \ifdim \UpperWidth > \LowerWidth
   3.196 -                % \UpperCenter > \LowerCenter
   3.197 -        \UpperAdjust=0pt
   3.198 -        \RuleAdjust=\UpperLeftOffset
   3.199 -        \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
   3.200 -        \RuleWidth=\UpperWidth
   3.201 -        \global\@LeftOffset=\LowerAdjust
   3.202 -%
   3.203 -        \else   % \UpperWidth <= \LowerWidth
   3.204 -        \ifdim \UpperCenter > \LowerCenter
   3.205 -%
   3.206 -        \UpperAdjust=0pt
   3.207 -        \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
   3.208 -        \LowerAdjust=\RuleAdjust
   3.209 -        \RuleWidth=\LowerWidth
   3.210 -        \global\@LeftOffset=\LowerAdjust
   3.211 -%
   3.212 -        \else   % \UpperWidth <= \LowerWidth
   3.213 -                % \UpperCenter <= \LowerCenter
   3.214 -%
   3.215 -        \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
   3.216 -        \RuleAdjust=0pt
   3.217 -        \LowerAdjust=0pt
   3.218 -        \RuleWidth=\LowerWidth
   3.219 -        \global\@LeftOffset=0pt
   3.220 -%
   3.221 -        \fi\fi
   3.222 -% Make a box
   3.223 -        \if@inferRule
   3.224 -%
   3.225 -        \setbox\ResultBox=\vbox{
   3.226 -                \moveright \UpperAdjust \box\@UpperPart
   3.227 -                \nointerlineskip \kern\inferLineSkip
   3.228 -                \if@DoubleRule
   3.229 -                \moveright \RuleAdjust \vbox{\hrule width\RuleWidth
   3.230 -                        \kern 1pt\hrule width\RuleWidth}\relax
   3.231 -                \else
   3.232 -                \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
   3.233 -                \fi
   3.234 -                \nointerlineskip \kern\inferLineSkip
   3.235 -                \moveright \LowerAdjust \box\@LowerPart }\relax
   3.236 -%
   3.237 -        \@ifEmpty{#1}{}{\relax
   3.238 -%
   3.239 -        \HLabelAdjust=\wd\ResultBox     \advance\HLabelAdjust by -\RuleAdjust
   3.240 -        \advance\HLabelAdjust by -\RuleWidth
   3.241 -        \WidthAdjust=\HLabelAdjust
   3.242 -        \advance\WidthAdjust by -\inferLabelSkip
   3.243 -        \advance\WidthAdjust by -\wd\@LabelPart
   3.244 -        \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
   3.245 -%
   3.246 -        \VLabelAdjust=\dp\@LabelPart
   3.247 -        \advance\VLabelAdjust by -\ht\@LabelPart
   3.248 -        \VLabelAdjust=0.5\VLabelAdjust  \advance\VLabelAdjust by \LowerHeight
   3.249 -        \advance\VLabelAdjust by \inferLineSkip
   3.250 -%
   3.251 -        \setbox\ResultBox=\hbox{\box\ResultBox
   3.252 -                \kern -\HLabelAdjust \kern\inferLabelSkip
   3.253 -                \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
   3.254 -%
   3.255 -        }\relax % end @ifEmpty
   3.256 -%
   3.257 -        \else % \@inferRulefalse
   3.258 -%
   3.259 -        \setbox\ResultBox=\vbox{
   3.260 -                \moveright \UpperAdjust \box\@UpperPart
   3.261 -                \nointerlineskip \kern\inferLineSkip
   3.262 -                \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
   3.263 -                        \@ifEmpty{#1}{}{\relax
   3.264 -                        \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
   3.265 -        \fi
   3.266 -%
   3.267 -        \global\@RightOffset=\wd\ResultBox
   3.268 -        \global\advance\@RightOffset by -\@LeftOffset
   3.269 -        \global\advance\@RightOffset by -\LowerWidth
   3.270 -        \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
   3.271 -%
   3.272 -        \box\ResultBox
   3.273 -        \@RestoreMath
   3.274 -}
   3.275 -\endinput
     4.1 --- a/doc-src/TutorialI/tutorial.tex	Mon Nov 27 11:06:28 2000 +0100
     4.2 +++ b/doc-src/TutorialI/tutorial.tex	Mon Nov 27 16:40:56 2000 +0100
     4.3 @@ -3,7 +3,7 @@
     4.4  \remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
     4.5  \usepackage{cl2emono-modified,isabelle,isabellesym}
     4.6  \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
     4.7 -\usepackage{proof,amsmath}
     4.8 +\usepackage{../proof,amsmath}
     4.9  \usepackage{../pdfsetup}    %last package!
    4.10  
    4.11  %\newtheorem{theorem}{Theorem}[section]