updated;
authorwenzelm
Wed Oct 18 23:58:07 2000 +0200 (2000-10-18)
changeset 10267325ead6d9457
parent 10266 41f6be79b44f
child 10268 ca52783f9801
updated;
doc-src/AxClass/generated/isabelle.sty
doc-src/TutorialI/CTL/document/CTLind.tex
doc-src/TutorialI/Misc/document/Tree2.tex
doc-src/TutorialI/Misc/document/arith1.tex
doc-src/TutorialI/Misc/document/arith2.tex
doc-src/TutorialI/Misc/document/arith3.tex
doc-src/TutorialI/Misc/document/case_exprs.tex
doc-src/TutorialI/Misc/document/prime_def.tex
doc-src/TutorialI/Recdef/document/Nested0.tex
doc-src/TutorialI/Recdef/document/Nested1.tex
doc-src/TutorialI/Recdef/document/Nested2.tex
doc-src/TutorialI/Trie/document/Option2.tex
doc-src/TutorialI/isabelle.sty
     1.1 --- a/doc-src/AxClass/generated/isabelle.sty	Wed Oct 18 23:44:52 2000 +0200
     1.2 +++ b/doc-src/AxClass/generated/isabelle.sty	Wed Oct 18 23:58:07 2000 +0200
     1.3 @@ -23,8 +23,8 @@
     1.4  \newcommand{\isamath}[1]{\emph{$#1$}}
     1.5  \newcommand{\isatext}[1]{\emph{#1}}
     1.6  \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
     1.7 -\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}_{#1}$}}
     1.8 -\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}^{#1}$}}
     1.9 +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    1.10 +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    1.11  
    1.12  \newdimen\isa@parindent\newdimen\isa@parskip
    1.13  
    1.14 @@ -141,7 +141,7 @@
    1.15  \renewcommand{\isacharbraceleft}{\isamath{\{}}%
    1.16  \renewcommand{\isacharbar}{\isamath{\mid}}%
    1.17  \renewcommand{\isacharbraceright}{\isamath{\}}}%
    1.18 -\renewcommand{\isachartilde}{\isamath{{}^\sim}}%
    1.19 +\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
    1.20  }
    1.21  
    1.22  \newcommand{\isabellestylesl}{%
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Wed Oct 18 23:58:07 2000 +0200
     2.3 @@ -0,0 +1,134 @@
     2.4 +%
     2.5 +\begin{isabellebody}%
     2.6 +\def\isabellecontext{CTLind}%
     2.7 +%
     2.8 +\isamarkupsubsection{CTL revisited}
     2.9 +%
    2.10 +\begin{isamarkuptext}%
    2.11 +\label{sec:CTL-revisited}
    2.12 +In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
    2.13 +model checker for CTL. In particular the proof of the
    2.14 +\isa{infinity{\isacharunderscore}lemma} on the way to \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} is not as
    2.15 +simple as one might intuitively expect, due to the \isa{SOME} operator
    2.16 +involved. The purpose of this section is to show how an inductive definition
    2.17 +can help to simplify the proof of \isa{AF{\isacharunderscore}lemma{\isadigit{2}}}.
    2.18 +
    2.19 +Let us call a (finite or infinite) path \emph{\isa{A}-avoiding} if it does
    2.20 +not touch any node in the set \isa{A}. Then \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} says
    2.21 +that if no infinite path from some state \isa{s} is \isa{A}-avoiding,
    2.22 +then \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. We prove this by inductively defining the set
    2.23 +\isa{Avoid\ s\ A} of states reachable from \isa{s} by a finite \isa{A}-avoiding path:
    2.24 +% Second proof of opposite direction, directly by well-founded induction
    2.25 +% on the initial segment of M that avoids A.%
    2.26 +\end{isamarkuptext}%
    2.27 +\isacommand{consts}\ Avoid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline
    2.28 +\isacommand{inductive}\ {\isachardoublequote}Avoid\ s\ A{\isachardoublequote}\isanewline
    2.29 +\isakeyword{intros}\ {\isachardoublequote}s\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}\isanewline
    2.30 +\ \ \ \ \ \ \ {\isachardoublequote}{\isasymlbrakk}\ t\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\ t\ {\isasymnotin}\ A{\isacharsemicolon}\ {\isacharparenleft}t{\isacharcomma}u{\isacharparenright}\ {\isasymin}\ M\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ u\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}%
    2.31 +\begin{isamarkuptext}%
    2.32 +It is easy to see that for any infinite \isa{A}-avoiding path \isa{f}
    2.33 +with \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path
    2.34 +starting with \isa{s} because (by definition of \isa{Avoid}) there is a
    2.35 +finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isadigit{0}}}.
    2.36 +The proof is by induction on \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A}. However,
    2.37 +this requires the following
    2.38 +reformulation, as explained in \S\ref{sec:ind-var-in-prems} above;
    2.39 +the \isa{rule{\isacharunderscore}format} directive undoes the reformulation after the proof.%
    2.40 +\end{isamarkuptext}%
    2.41 +\isacommand{lemma}\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
    2.42 +\ \ {\isachardoublequote}t\ {\isasymin}\ Avoid\ s\ A\ \ {\isasymLongrightarrow}\isanewline
    2.43 +\ \ \ {\isasymforall}f{\isasymin}Paths\ t{\isachardot}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ f\ i\ {\isasymnotin}\ A{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A{\isacharparenright}{\isachardoublequote}\isanewline
    2.44 +\isacommand{apply}{\isacharparenleft}erule\ Avoid{\isachardot}induct{\isacharparenright}\isanewline
    2.45 +\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
    2.46 +\isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
    2.47 +\isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ case\ i\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ t\ {\isacharbar}\ Suc\ i\ {\isasymRightarrow}\ f\ i{\isachardoublequote}\ \isakeyword{in}\ bspec{\isacharparenright}\isanewline
    2.48 +\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}Paths{\isacharunderscore}def\ split{\isacharcolon}nat{\isachardot}split{\isacharparenright}\isanewline
    2.49 +\isacommand{done}%
    2.50 +\begin{isamarkuptext}%
    2.51 +\noindent
    2.52 +The base case (\isa{t\ {\isacharequal}\ s}) is trivial (\isa{blast}).
    2.53 +In the induction step, we have an infinite \isa{A}-avoiding path \isa{f}
    2.54 +starting from \isa{u}, a successor of \isa{t}. Now we simply instantiate
    2.55 +the \isa{{\isasymforall}f{\isasymin}Paths\ t} in the induction hypothesis by the path starting with
    2.56 +\isa{t} and continuing with \isa{f}. That is what the above $\lambda$-term
    2.57 +expresses. That fact that this is a path starting with \isa{t} and that
    2.58 +the instantiated induction hypothesis implies the conclusion is shown by
    2.59 +simplification.
    2.60 +
    2.61 +Now we come to the key lemma. It says that if \isa{t} can be reached by a
    2.62 +finite \isa{A}-avoiding path from \isa{s}, then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}},
    2.63 +provided there is no infinite \isa{A}-avoiding path starting from \isa{s}.%
    2.64 +\end{isamarkuptext}%
    2.65 +\isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline
    2.66 +\ \ {\isachardoublequote}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ t\ {\isasymin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}%
    2.67 +\begin{isamarkuptxt}%
    2.68 +\noindent
    2.69 +The trick is not to induct on \isa{t\ {\isasymin}\ Avoid\ s\ A}, as already the base
    2.70 +case would be a problem, but to proceed by well-founded induction \isa{t}. Hence \isa{t\ {\isasymin}\ Avoid\ s\ A} needs to be brought into the conclusion as
    2.71 +well, which the directive \isa{rule{\isacharunderscore}format} undoes at the end (see below).
    2.72 +But induction with respect to which well-founded relation? The restriction
    2.73 +of \isa{M} to \isa{Avoid\ s\ A}:
    2.74 +\begin{isabelle}%
    2.75 +\ \ \ \ \ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}%
    2.76 +\end{isabelle}
    2.77 +As we shall see in a moment, the absence of infinite \isa{A}-avoiding paths
    2.78 +starting from \isa{s} implies well-foundedness of this relation. For the
    2.79 +moment we assume this and proceed with the induction:%
    2.80 +\end{isamarkuptxt}%
    2.81 +\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\isanewline
    2.82 +\ \ {\isachardoublequote}wf{\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isasymin}M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}{\isachardoublequote}{\isacharparenright}\isanewline
    2.83 +\ \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline
    2.84 +\ \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
    2.85 +\begin{isamarkuptxt}%
    2.86 +\noindent
    2.87 +Now can assume additionally (induction hypothesis) that if \isa{t\ {\isasymnotin}\ A}
    2.88 +then all successors of \isa{t} that are in \isa{Avoid\ s\ A} are in
    2.89 +\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. To prove the actual goal we unfold \isa{lfp} once. Now
    2.90 +we have to prove that \isa{t} is in \isa{A} or all successors of \isa{t} are in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. If \isa{t} is not in \isa{A}, the second
    2.91 +\isa{Avoid}-rule implies that all successors of \isa{t} are in
    2.92 +\isa{Avoid\ s\ A} (because we also assume \isa{t\ {\isasymin}\ Avoid\ s\ A}), and
    2.93 +hence, by the induction hypothesis, all successors of \isa{t} are indeed in
    2.94 +\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Mechanically:%
    2.95 +\end{isamarkuptxt}%
    2.96 +\ \isacommand{apply}{\isacharparenleft}rule\ ssubst\ {\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
    2.97 +\ \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
    2.98 +\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}%
    2.99 +\begin{isamarkuptxt}%
   2.100 +Having proved the main goal we return to the proof obligation that the above
   2.101 +relation is indeed well-founded. This is proved by contraposition: we assume
   2.102 +the relation is not well-founded. Thus there exists an infinite \isa{A}-avoiding path all in \isa{Avoid\ s\ A}, by theorem
   2.103 +\isa{wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain}:
   2.104 +\begin{isabelle}%
   2.105 +\ \ \ \ \ wf\ r\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ {\isacharparenleft}{\isasymexists}f{\isachardot}\ {\isasymforall}i{\isachardot}\ {\isacharparenleft}f\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharcomma}\ f\ i{\isacharparenright}\ {\isasymin}\ r{\isacharparenright}{\isacharparenright}%
   2.106 +\end{isabelle}
   2.107 +From lemma \isa{ex{\isacharunderscore}infinite{\isacharunderscore}path} the existence of an infinite
   2.108 +\isa{A}-avoiding path starting in \isa{s} follows, just as required for
   2.109 +the contraposition.%
   2.110 +\end{isamarkuptxt}%
   2.111 +\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline
   2.112 +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline
   2.113 +\isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
   2.114 +\isacommand{apply}{\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline
   2.115 +\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline
   2.116 +\isacommand{done}%
   2.117 +\begin{isamarkuptext}%
   2.118 +The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive means
   2.119 +that the assumption is left unchanged---otherwise the \isa{{\isasymforall}p} is turned
   2.120 +into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is,
   2.121 +\isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now
   2.122 +\begin{isabelle}%
   2.123 +\ \ \ \ \ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\ t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}%
   2.124 +\end{isabelle}
   2.125 +The main theorem is simply the corollary where \isa{t\ {\isacharequal}\ s},
   2.126 +in which case the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true
   2.127 +by the first \isa{Avoid}-rule). Isabelle confirms this:%
   2.128 +\end{isamarkuptext}%
   2.129 +\isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\isanewline
   2.130 +\ \ {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
   2.131 +\isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isanewline
   2.132 +\isanewline
   2.133 +\end{isabellebody}%
   2.134 +%%% Local Variables:
   2.135 +%%% mode: latex
   2.136 +%%% TeX-master: "root"
   2.137 +%%% End:
     3.1 --- a/doc-src/TutorialI/Misc/document/Tree2.tex	Wed Oct 18 23:44:52 2000 +0200
     3.2 +++ b/doc-src/TutorialI/Misc/document/Tree2.tex	Wed Oct 18 23:58:07 2000 +0200
     3.3 @@ -1,6 +1,6 @@
     3.4  %
     3.5  \begin{isabellebody}%
     3.6 -\def\isabellecontext{Tree2}%
     3.7 +\def\isabellecontext{Tree{\isadigit{2}}}%
     3.8  %
     3.9  \begin{isamarkuptext}%
    3.10  \noindent In Exercise~\ref{ex:Tree} we defined a function
     4.1 --- a/doc-src/TutorialI/Misc/document/arith1.tex	Wed Oct 18 23:44:52 2000 +0200
     4.2 +++ b/doc-src/TutorialI/Misc/document/arith1.tex	Wed Oct 18 23:58:07 2000 +0200
     4.3 @@ -1,6 +1,6 @@
     4.4  %
     4.5  \begin{isabellebody}%
     4.6 -\def\isabellecontext{arith1}%
     4.7 +\def\isabellecontext{arith{\isadigit{1}}}%
     4.8  \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
     4.9  \end{isabellebody}%
    4.10  %%% Local Variables:
     5.1 --- a/doc-src/TutorialI/Misc/document/arith2.tex	Wed Oct 18 23:44:52 2000 +0200
     5.2 +++ b/doc-src/TutorialI/Misc/document/arith2.tex	Wed Oct 18 23:58:07 2000 +0200
     5.3 @@ -1,6 +1,6 @@
     5.4  %
     5.5  \begin{isabellebody}%
     5.6 -\def\isabellecontext{arith2}%
     5.7 +\def\isabellecontext{arith{\isadigit{2}}}%
     5.8  \isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
     5.9  \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
    5.10  \end{isabellebody}%
     6.1 --- a/doc-src/TutorialI/Misc/document/arith3.tex	Wed Oct 18 23:44:52 2000 +0200
     6.2 +++ b/doc-src/TutorialI/Misc/document/arith3.tex	Wed Oct 18 23:58:07 2000 +0200
     6.3 @@ -1,6 +1,6 @@
     6.4  %
     6.5  \begin{isabellebody}%
     6.6 -\def\isabellecontext{arith3}%
     6.7 +\def\isabellecontext{arith{\isadigit{3}}}%
     6.8  \isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}\isanewline
     6.9  \end{isabellebody}%
    6.10  %%% Local Variables:
     7.1 --- a/doc-src/TutorialI/Misc/document/case_exprs.tex	Wed Oct 18 23:44:52 2000 +0200
     7.2 +++ b/doc-src/TutorialI/Misc/document/case_exprs.tex	Wed Oct 18 23:58:07 2000 +0200
     7.3 @@ -1,6 +1,6 @@
     7.4  %
     7.5  \begin{isabellebody}%
     7.6 -\def\isabellecontext{case_exprs}%
     7.7 +\def\isabellecontext{case{\isacharunderscore}exprs}%
     7.8  %
     7.9  \isamarkupsubsection{Case expressions}
    7.10  %
     8.1 --- a/doc-src/TutorialI/Misc/document/prime_def.tex	Wed Oct 18 23:44:52 2000 +0200
     8.2 +++ b/doc-src/TutorialI/Misc/document/prime_def.tex	Wed Oct 18 23:58:07 2000 +0200
     8.3 @@ -1,6 +1,6 @@
     8.4  %
     8.5  \begin{isabellebody}%
     8.6 -\def\isabellecontext{prime_def}%
     8.7 +\def\isabellecontext{prime{\isacharunderscore}def}%
     8.8  %
     8.9  \begin{isamarkuptext}%
    8.10  \begin{warn}
     9.1 --- a/doc-src/TutorialI/Recdef/document/Nested0.tex	Wed Oct 18 23:44:52 2000 +0200
     9.2 +++ b/doc-src/TutorialI/Recdef/document/Nested0.tex	Wed Oct 18 23:58:07 2000 +0200
     9.3 @@ -1,6 +1,6 @@
     9.4  %
     9.5  \begin{isabellebody}%
     9.6 -\def\isabellecontext{Nested0}%
     9.7 +\def\isabellecontext{Nested{\isadigit{0}}}%
     9.8  %
     9.9  \begin{isamarkuptext}%
    9.10  In \S\ref{sec:nested-datatype} we defined the datatype of terms%
    10.1 --- a/doc-src/TutorialI/Recdef/document/Nested1.tex	Wed Oct 18 23:44:52 2000 +0200
    10.2 +++ b/doc-src/TutorialI/Recdef/document/Nested1.tex	Wed Oct 18 23:58:07 2000 +0200
    10.3 @@ -1,6 +1,6 @@
    10.4  %
    10.5  \begin{isabellebody}%
    10.6 -\def\isabellecontext{Nested1}%
    10.7 +\def\isabellecontext{Nested{\isadigit{1}}}%
    10.8  %
    10.9  \begin{isamarkuptext}%
   10.10  \noindent
    11.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Wed Oct 18 23:44:52 2000 +0200
    11.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Wed Oct 18 23:58:07 2000 +0200
    11.3 @@ -1,6 +1,6 @@
    11.4  %
    11.5  \begin{isabellebody}%
    11.6 -\def\isabellecontext{Nested2}%
    11.7 +\def\isabellecontext{Nested{\isadigit{2}}}%
    11.8  %
    11.9  \begin{isamarkuptext}%
   11.10  \noindent
    12.1 --- a/doc-src/TutorialI/Trie/document/Option2.tex	Wed Oct 18 23:44:52 2000 +0200
    12.2 +++ b/doc-src/TutorialI/Trie/document/Option2.tex	Wed Oct 18 23:58:07 2000 +0200
    12.3 @@ -1,6 +1,6 @@
    12.4  %
    12.5  \begin{isabellebody}%
    12.6 -\def\isabellecontext{Option2}%
    12.7 +\def\isabellecontext{Option{\isadigit{2}}}%
    12.8  \isanewline
    12.9  \isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabellebody}%
   12.10  %%% Local Variables:
    13.1 --- a/doc-src/TutorialI/isabelle.sty	Wed Oct 18 23:44:52 2000 +0200
    13.2 +++ b/doc-src/TutorialI/isabelle.sty	Wed Oct 18 23:58:07 2000 +0200
    13.3 @@ -23,8 +23,8 @@
    13.4  \newcommand{\isamath}[1]{\emph{$#1$}}
    13.5  \newcommand{\isatext}[1]{\emph{#1}}
    13.6  \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    13.7 -\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}_{#1}$}}
    13.8 -\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}^{#1}$}}
    13.9 +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
   13.10 +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
   13.11  
   13.12  \newdimen\isa@parindent\newdimen\isa@parskip
   13.13  
   13.14 @@ -141,7 +141,7 @@
   13.15  \renewcommand{\isacharbraceleft}{\isamath{\{}}%
   13.16  \renewcommand{\isacharbar}{\isamath{\mid}}%
   13.17  \renewcommand{\isacharbraceright}{\isamath{\}}}%
   13.18 -\renewcommand{\isachartilde}{\isamath{{}^\sim}}%
   13.19 +\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
   13.20  }
   13.21  
   13.22  \newcommand{\isabellestylesl}{%