# HG changeset patch
# User nipkow
# Date 975339656 -3600
# Node ID 270b285d48ee48f3c9d921355f222530fb880cc6
# Parent  68105cf615fa7eeaac80a7ce9ffc3510688e27a3
*** empty log message ***

diff -r 68105cf615fa -r 270b285d48ee doc-src/TutorialI/CTL/PDL.thy
--- a/doc-src/TutorialI/CTL/PDL.thy	Mon Nov 27 11:06:28 2000 +0100
+++ b/doc-src/TutorialI/CTL/PDL.thy	Mon Nov 27 16:40:56 2000 +0100
@@ -96,7 +96,7 @@
 
 apply(rule equalityI);
  apply(rule subsetI);
- apply(simp)
+ apply(simp)(*<*)apply(rename_tac s)(*>*)
 
 txt{*\noindent
 Simplification leaves us with the following first subgoal
diff -r 68105cf615fa -r 270b285d48ee doc-src/TutorialI/CTL/document/PDL.tex
--- a/doc-src/TutorialI/CTL/document/PDL.tex	Mon Nov 27 11:06:28 2000 +0100
+++ b/doc-src/TutorialI/CTL/document/PDL.tex	Mon Nov 27 16:40:56 2000 +0100
@@ -98,7 +98,7 @@
 \noindent
 Simplification leaves us with the following first subgoal
 \begin{isabelle}%
-\ {\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%
+\ {\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%
 \end{isabelle}
 which is proved by \isa{lfp}-induction:%
 \end{isamarkuptxt}%
diff -r 68105cf615fa -r 270b285d48ee doc-src/TutorialI/proof.sty
--- a/doc-src/TutorialI/proof.sty	Mon Nov 27 11:06:28 2000 +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
diff -r 68105cf615fa -r 270b285d48ee doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Mon Nov 27 11:06:28 2000 +0100
+++ b/doc-src/TutorialI/tutorial.tex	Mon Nov 27 16:40:56 2000 +0100
@@ -3,7 +3,7 @@
 \remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
 \usepackage{cl2emono-modified,isabelle,isabellesym}
 \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
-\usepackage{proof,amsmath}
+\usepackage{../proof,amsmath}
 \usepackage{../pdfsetup}    %last package!
 
 %\newtheorem{theorem}{Theorem}[section]