updated;
authorwenzelm
Mon Sep 11 18:00:47 2000 +0200 (2000-09-11)
changeset 99243370f6aa3200
parent 9923 fe13743ffc8b
child 9925 40f02ebcb3c0
updated;
doc-src/TutorialI/CodeGen/document/CodeGen.tex
doc-src/TutorialI/Datatype/document/ABexpr.tex
doc-src/TutorialI/Datatype/document/Fundata.tex
doc-src/TutorialI/Datatype/document/Nested.tex
doc-src/TutorialI/Datatype/document/unfoldnested.tex
doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
doc-src/TutorialI/Misc/document/AdvancedInd.tex
doc-src/TutorialI/Misc/document/Itrev.tex
doc-src/TutorialI/Misc/document/Tree.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/fakenat.tex
doc-src/TutorialI/Misc/document/natsum.tex
doc-src/TutorialI/Misc/document/pairs.tex
doc-src/TutorialI/Misc/document/prime_def.tex
doc-src/TutorialI/Misc/document/simp.tex
doc-src/TutorialI/Misc/document/types.tex
doc-src/TutorialI/Recdef/document/Induction.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/Recdef/document/examples.tex
doc-src/TutorialI/Recdef/document/simplification.tex
doc-src/TutorialI/Recdef/document/termination.tex
doc-src/TutorialI/ToyList/document/ToyList.tex
doc-src/TutorialI/Trie/document/Option2.tex
doc-src/TutorialI/Trie/document/Trie.tex
doc-src/TutorialI/isabelle.sty
     1.1 --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Mon Sep 11 17:59:53 2000 +0200
     1.2 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Mon Sep 11 18:00:47 2000 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4  %
     1.5  \begin{isabellebody}%
     1.6 +\def\isabellecontext{CodeGen}%
     1.7  %
     1.8  \isamarkupsection{Case study: compiling expressions}
     1.9  %
     2.1 --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Mon Sep 11 17:59:53 2000 +0200
     2.2 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Mon Sep 11 18:00:47 2000 +0200
     2.3 @@ -1,5 +1,6 @@
     2.4  %
     2.5  \begin{isabellebody}%
     2.6 +\def\isabellecontext{ABexpr}%
     2.7  %
     2.8  \begin{isamarkuptext}%
     2.9  Sometimes it is necessary to define two datatypes that depend on each
     3.1 --- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Sep 11 17:59:53 2000 +0200
     3.2 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Sep 11 18:00:47 2000 +0200
     3.3 @@ -1,5 +1,6 @@
     3.4  %
     3.5  \begin{isabellebody}%
     3.6 +\def\isabellecontext{Fundata}%
     3.7  \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Branch\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}%
     3.8  \begin{isamarkuptext}%
     3.9  \noindent
    3.10 @@ -10,11 +11,9 @@
    3.11  \isa{nat}, we have an infinitely branching tree because each node
    3.12  has as many subtrees as there are natural numbers. How can we possibly
    3.13  write down such a tree? Using functional notation! For example, the term
    3.14 -%
    3.15  \begin{isabelle}%
    3.16  \ \ \ \ \ Branch\ \isadigit{0}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Branch\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
    3.17 -\end{isabelle}%
    3.18 -
    3.19 +\end{isabelle}
    3.20  of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose
    3.21  root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
    3.22  has merely \isa{Tip}s as further subtrees.
     4.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Sep 11 17:59:53 2000 +0200
     4.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Sep 11 18:00:47 2000 +0200
     4.3 @@ -1,5 +1,6 @@
     4.4  %
     4.5  \begin{isabellebody}%
     4.6 +\def\isabellecontext{Nested}%
     4.7  %
     4.8  \begin{isamarkuptext}%
     4.9  So far, all datatypes had the property that on the right-hand side of their
    4.10 @@ -71,11 +72,9 @@
    4.11  \begin{exercise}
    4.12  The fact that substitution distributes over composition can be expressed
    4.13  roughly as follows:
    4.14 -%
    4.15  \begin{isabelle}%
    4.16  \ \ \ \ \ subst\ {\isacharparenleft}f\ o\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}%
    4.17 -\end{isabelle}%
    4.18 -
    4.19 +\end{isabelle}
    4.20  Correct this statement (you will find that it does not type-check),
    4.21  strengthen it, and prove it. (Note: \isaindexbold{o} is function composition;
    4.22  its definition is found in theorem \isa{o{\isacharunderscore}def}).
    4.23 @@ -89,11 +88,9 @@
    4.24  The experienced functional programmer may feel that our above definition of
    4.25  \isa{subst} is unnecessarily complicated in that \isa{substs} is
    4.26  completely unnecessary. The \isa{App}-case can be defined directly as
    4.27 -%
    4.28  \begin{isabelle}%
    4.29  \ \ \ \ \ subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}%
    4.30 -\end{isabelle}%
    4.31 -
    4.32 +\end{isabelle}
    4.33  where \isa{map} is the standard list function such that
    4.34  \isa{map\ f\ {\isacharbrackleft}x\isadigit{1}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}xn{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}f\ x\isadigit{1}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}f\ xn{\isacharbrackright}}. This is true, but Isabelle
    4.35  insists on the above fixed format. Fortunately, we can easily \emph{prove}
     5.1 --- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Mon Sep 11 17:59:53 2000 +0200
     5.2 +++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Mon Sep 11 18:00:47 2000 +0200
     5.3 @@ -1,5 +1,6 @@
     5.4  %
     5.5  \begin{isabellebody}%
     5.6 +\def\isabellecontext{unfoldnested}%
     5.7  \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}a\ {\isacharbar}\ App\ {\isacharprime}b\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\isanewline
     5.8  \isakeyword{and}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\end{isabellebody}%
     5.9  %%% Local Variables:
     6.1 --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Mon Sep 11 17:59:53 2000 +0200
     6.2 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Mon Sep 11 18:00:47 2000 +0200
     6.3 @@ -1,5 +1,6 @@
     6.4  %
     6.5  \begin{isabellebody}%
     6.6 +\def\isabellecontext{Ifexpr}%
     6.7  %
     6.8  \begin{isamarkuptext}%
     6.9  \subsubsection{How can we model boolean expressions?}
     7.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Sep 11 17:59:53 2000 +0200
     7.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Sep 11 18:00:47 2000 +0200
     7.3 @@ -1,5 +1,6 @@
     7.4  %
     7.5  \begin{isabellebody}%
     7.6 +\def\isabellecontext{AdvancedInd}%
     7.7  %
     7.8  \begin{isamarkuptext}%
     7.9  \noindent
    7.10 @@ -85,16 +86,16 @@
    7.11  \begin{isamarkuptext}%
    7.12  \noindent
    7.13  or the wholesale stripping of \isa{{\isasymforall}} and
    7.14 -\isa{{\isasymlongrightarrow}} in the conclusion via \isa{rulify}%
    7.15 +\isa{{\isasymlongrightarrow}} in the conclusion via \isa{rulified}%
    7.16  \end{isamarkuptext}%
    7.17 -\isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}rulify{\isacharbrackright}%
    7.18 +\isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}rulified{\isacharbrackright}%
    7.19  \begin{isamarkuptext}%
    7.20  \noindent
    7.21  yielding \isa{{\isasymlbrakk}A\ y{\isacharsemicolon}\ B\ y{\isasymrbrakk}\ {\isasymLongrightarrow}\ B\ y\ {\isasymand}\ A\ y}.
    7.22  You can go one step further and include these derivations already in the
    7.23  statement of your original lemma, thus avoiding the intermediate step:%
    7.24  \end{isamarkuptext}%
    7.25 -\isacommand{lemma}\ myrule{\isacharbrackleft}rulify{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}%
    7.26 +\isacommand{lemma}\ myrule{\isacharbrackleft}rulified{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}%
    7.27  \begin{isamarkuptext}%
    7.28  \bigskip
    7.29  
    7.30 @@ -119,12 +120,10 @@
    7.31  Structural induction on \isa{nat} is
    7.32  usually known as ``mathematical induction''. There is also ``complete
    7.33  induction'', where you must prove $P(n)$ under the assumption that $P(m)$
    7.34 -holds for all $m<n$. In Isabelle, this is the theorem \isa{less{\isacharunderscore}induct}:
    7.35 -%
    7.36 +holds for all $m<n$. In Isabelle, this is the theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}:
    7.37  \begin{isabelle}%
    7.38  \ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
    7.39 -\end{isabelle}%
    7.40 -
    7.41 +\end{isabelle}
    7.42  Here is an example of its application.%
    7.43  \end{isamarkuptext}%
    7.44  \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isacharequal}{\isachargreater}\ nat{\isachardoublequote}\isanewline
    7.45 @@ -142,11 +141,11 @@
    7.46  \isacommand{lemma}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}%
    7.47  \begin{isamarkuptxt}%
    7.48  \noindent
    7.49 -To perform induction on \isa{k} using \isa{less{\isacharunderscore}induct}, we use the same
    7.50 +To perform induction on \isa{k} using \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}, we use the same
    7.51  general induction method as for recursion induction (see
    7.52  \S\ref{sec:recdef-induction}):%
    7.53  \end{isamarkuptxt}%
    7.54 -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ k\ rule{\isacharcolon}less{\isacharunderscore}induct{\isacharparenright}%
    7.55 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ k\ rule{\isacharcolon}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharparenright}%
    7.56  \begin{isamarkuptxt}%
    7.57  \noindent
    7.58  which leaves us with the following proof state:
    7.59 @@ -163,7 +162,7 @@
    7.60  \ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
    7.61  \end{isabelle}%
    7.62  \end{isamarkuptxt}%
    7.63 -\isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}%
    7.64 +\isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}%
    7.65  \begin{isamarkuptext}%
    7.66  \noindent
    7.67  It is not surprising if you find the last step puzzling.
    7.68 @@ -186,13 +185,13 @@
    7.69  
    7.70  We can now derive the desired \isa{i\ {\isasymle}\ f\ i} from \isa{f{\isacharunderscore}incr}:%
    7.71  \end{isamarkuptext}%
    7.72 -\isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rulify{\isacharcomma}\ OF\ refl{\isacharbrackright}%
    7.73 +\isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rulified{\isacharcomma}\ OF\ refl{\isacharbrackright}%
    7.74  \begin{isamarkuptext}%
    7.75  \noindent
    7.76  The final \isa{refl} gets rid of the premise \isa{{\isacharquery}k\ {\isacharequal}\ f\ {\isacharquery}i}. Again,
    7.77  we could have included this derivation in the original statement of the lemma:%
    7.78  \end{isamarkuptext}%
    7.79 -\isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rulify{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}%
    7.80 +\isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rulified{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}%
    7.81  \begin{isamarkuptext}%
    7.82  \begin{exercise}
    7.83  From the above axiom and lemma for \isa{f} show that \isa{f} is the
    7.84 @@ -220,7 +219,7 @@
    7.85  \label{sec:derive-ind}
    7.86  Induction schemas are ordinary theorems and you can derive new ones
    7.87  whenever you wish.  This section shows you how to, using the example
    7.88 -of \isa{less{\isacharunderscore}induct}. Assume we only have structural induction
    7.89 +of \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}. Assume we only have structural induction
    7.90  available for \isa{nat} and want to derive complete induction. This
    7.91  requires us to generalize the statement first:%
    7.92  \end{isamarkuptext}%
    7.93 @@ -240,32 +239,28 @@
    7.94  \begin{isamarkuptext}%
    7.95  \noindent
    7.96  The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction:
    7.97 -%
    7.98  \begin{isabelle}%
    7.99  \ \ \ \ \ {\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
   7.100 -\end{isabelle}%
   7.101 -
   7.102 +\end{isabelle}
   7.103  
   7.104  Now it is straightforward to derive the original version of
   7.105 -\isa{less{\isacharunderscore}induct} by manipulting the conclusion of the above lemma:
   7.106 +\isa{nat{\isacharunderscore}less{\isacharunderscore}induct} by manipulting the conclusion of the above lemma:
   7.107  instantiate \isa{n} by \isa{Suc\ n} and \isa{m} by \isa{n} and
   7.108  remove the trivial condition \isa{n\ {\isacharless}\ Sc\ n}. Fortunately, this
   7.109  happens automatically when we add the lemma as a new premise to the
   7.110  desired goal:%
   7.111  \end{isamarkuptext}%
   7.112 -\isacommand{theorem}\ less{\isacharunderscore}induct{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline
   7.113 +\isacommand{theorem}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline
   7.114  \isacommand{by}{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}%
   7.115  \begin{isamarkuptext}%
   7.116  \noindent
   7.117  Finally we should mention that HOL already provides the mother of all
   7.118  inductions, \emph{wellfounded induction} (\isa{wf{\isacharunderscore}induct}):
   7.119 -%
   7.120  \begin{isabelle}%
   7.121  \ \ \ \ \ {\isasymlbrakk}wf\ r{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isasymforall}y{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r\ {\isasymlongrightarrow}\ P\ y\ {\isasymLongrightarrow}\ P\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ a%
   7.122 -\end{isabelle}%
   7.123 -
   7.124 +\end{isabelle}
   7.125  where \isa{wf\ r} means that the relation \isa{r} is wellfounded.
   7.126 -For example \isa{less{\isacharunderscore}induct} is the special case where \isa{r} is
   7.127 +For example \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} is the special case where \isa{r} is
   7.128  \isa{{\isacharless}} on \isa{nat}. For details see the library.%
   7.129  \end{isamarkuptext}%
   7.130  \end{isabellebody}%
     8.1 --- a/doc-src/TutorialI/Misc/document/Itrev.tex	Mon Sep 11 17:59:53 2000 +0200
     8.2 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Mon Sep 11 18:00:47 2000 +0200
     8.3 @@ -1,5 +1,6 @@
     8.4  %
     8.5  \begin{isabellebody}%
     8.6 +\def\isabellecontext{Itrev}%
     8.7  %
     8.8  \isamarkupsection{Induction heuristics}
     8.9  %
     9.1 --- a/doc-src/TutorialI/Misc/document/Tree.tex	Mon Sep 11 17:59:53 2000 +0200
     9.2 +++ b/doc-src/TutorialI/Misc/document/Tree.tex	Mon Sep 11 18:00:47 2000 +0200
     9.3 @@ -1,5 +1,6 @@
     9.4  %
     9.5  \begin{isabellebody}%
     9.6 +\def\isabellecontext{Tree}%
     9.7  %
     9.8  \begin{isamarkuptext}%
     9.9  \noindent
    10.1 --- a/doc-src/TutorialI/Misc/document/Tree2.tex	Mon Sep 11 17:59:53 2000 +0200
    10.2 +++ b/doc-src/TutorialI/Misc/document/Tree2.tex	Mon Sep 11 18:00:47 2000 +0200
    10.3 @@ -1,5 +1,6 @@
    10.4  %
    10.5  \begin{isabellebody}%
    10.6 +\def\isabellecontext{Tree2}%
    10.7  %
    10.8  \begin{isamarkuptext}%
    10.9  \noindent In Exercise~\ref{ex:Tree} we defined a function
    11.1 --- a/doc-src/TutorialI/Misc/document/arith1.tex	Mon Sep 11 17:59:53 2000 +0200
    11.2 +++ b/doc-src/TutorialI/Misc/document/arith1.tex	Mon Sep 11 18:00:47 2000 +0200
    11.3 @@ -1,5 +1,6 @@
    11.4  %
    11.5  \begin{isabellebody}%
    11.6 +\def\isabellecontext{arith1}%
    11.7  \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
    11.8  \end{isabellebody}%
    11.9  %%% Local Variables:
    12.1 --- a/doc-src/TutorialI/Misc/document/arith2.tex	Mon Sep 11 17:59:53 2000 +0200
    12.2 +++ b/doc-src/TutorialI/Misc/document/arith2.tex	Mon Sep 11 18:00:47 2000 +0200
    12.3 @@ -1,5 +1,6 @@
    12.4  %
    12.5  \begin{isabellebody}%
    12.6 +\def\isabellecontext{arith2}%
    12.7  \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
    12.8  \isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline
    12.9  \end{isabellebody}%
    13.1 --- a/doc-src/TutorialI/Misc/document/arith3.tex	Mon Sep 11 17:59:53 2000 +0200
    13.2 +++ b/doc-src/TutorialI/Misc/document/arith3.tex	Mon Sep 11 18:00:47 2000 +0200
    13.3 @@ -1,5 +1,6 @@
    13.4  %
    13.5  \begin{isabellebody}%
    13.6 +\def\isabellecontext{arith3}%
    13.7  \isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}\isadigit{0}\ {\isasymor}\ n{\isacharequal}\isadigit{1}{\isachardoublequote}\isanewline
    13.8  \end{isabellebody}%
    13.9  %%% Local Variables:
    14.1 --- a/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Sep 11 17:59:53 2000 +0200
    14.2 +++ b/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Sep 11 18:00:47 2000 +0200
    14.3 @@ -1,5 +1,6 @@
    14.4  %
    14.5  \begin{isabellebody}%
    14.6 +\def\isabellecontext{case_exprs}%
    14.7  %
    14.8  \isamarkupsubsection{Case expressions}
    14.9  %
   14.10 @@ -7,11 +8,9 @@
   14.11  \label{sec:case-expressions}
   14.12  HOL also features \isaindexbold{case}-expressions for analyzing
   14.13  elements of a datatype. For example,
   14.14 -%
   14.15  \begin{isabelle}%
   14.16  \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y%
   14.17 -\end{isabelle}%
   14.18 -
   14.19 +\end{isabelle}
   14.20  evaluates to \isa{\isadigit{1}} if \isa{xs} is \isa{{\isacharbrackleft}{\isacharbrackright}} and to \isa{y} if 
   14.21  \isa{xs} is \isa{y\ {\isacharhash}\ ys}. (Since the result in both branches must be of
   14.22  the same type, it follows that \isa{y} is of type \isa{nat} and hence
   14.23 @@ -36,18 +35,14 @@
   14.24  \noindent
   14.25  Nested patterns can be simulated by nested \isa{case}-expressions: instead
   14.26  of
   14.27 -%
   14.28  \begin{isabelle}%
   14.29  \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}{\isachargreater}\ \isadigit{1}\ {\isacharbar}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}{\isachargreater}\ x\ {\isacharbar}\ x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}\ {\isacharequal}{\isachargreater}\ y%
   14.30 -\end{isabelle}%
   14.31 -
   14.32 +\end{isabelle}
   14.33  write
   14.34 -%
   14.35  \begin{isabelle}%
   14.36  \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\isanewline
   14.37  \ \ \ \ \ {\isacharbar}\ x\ {\isacharhash}\ ys\ {\isasymRightarrow}\ case\ ys\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ x\ {\isacharbar}\ y\ {\isacharhash}\ zs\ {\isasymRightarrow}\ y%
   14.38 -\end{isabelle}%
   14.39 -
   14.40 +\end{isabelle}
   14.41  
   14.42  Note that \isa{case}-expressions may need to be enclosed in parentheses to
   14.43  indicate their scope%
    15.1 --- a/doc-src/TutorialI/Misc/document/fakenat.tex	Mon Sep 11 17:59:53 2000 +0200
    15.2 +++ b/doc-src/TutorialI/Misc/document/fakenat.tex	Mon Sep 11 18:00:47 2000 +0200
    15.3 @@ -1,5 +1,6 @@
    15.4  %
    15.5  \begin{isabellebody}%
    15.6 +\def\isabellecontext{fakenat}%
    15.7  %
    15.8  \begin{isamarkuptext}%
    15.9  \noindent
    16.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex	Mon Sep 11 17:59:53 2000 +0200
    16.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex	Mon Sep 11 18:00:47 2000 +0200
    16.3 @@ -1,14 +1,13 @@
    16.4  %
    16.5  \begin{isabellebody}%
    16.6 +\def\isabellecontext{natsum}%
    16.7  %
    16.8  \begin{isamarkuptext}%
    16.9  \noindent
   16.10  In particular, there are \isa{case}-expressions, for example
   16.11 -%
   16.12  \begin{isabelle}%
   16.13  \ \ \ \ \ case\ n\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m%
   16.14 -\end{isabelle}%
   16.15 -
   16.16 +\end{isabelle}
   16.17  primitive recursion, for example%
   16.18  \end{isamarkuptext}%
   16.19  \isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    17.1 --- a/doc-src/TutorialI/Misc/document/pairs.tex	Mon Sep 11 17:59:53 2000 +0200
    17.2 +++ b/doc-src/TutorialI/Misc/document/pairs.tex	Mon Sep 11 18:00:47 2000 +0200
    17.3 @@ -1,5 +1,6 @@
    17.4  %
    17.5  \begin{isabellebody}%
    17.6 +\def\isabellecontext{pairs}%
    17.7  %
    17.8  \begin{isamarkuptext}%
    17.9  HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ *
    18.1 --- a/doc-src/TutorialI/Misc/document/prime_def.tex	Mon Sep 11 17:59:53 2000 +0200
    18.2 +++ b/doc-src/TutorialI/Misc/document/prime_def.tex	Mon Sep 11 18:00:47 2000 +0200
    18.3 @@ -1,24 +1,21 @@
    18.4  %
    18.5  \begin{isabellebody}%
    18.6 +\def\isabellecontext{prime_def}%
    18.7  %
    18.8  \begin{isamarkuptext}%
    18.9  \begin{warn}
   18.10  A common mistake when writing definitions is to introduce extra free
   18.11  variables on the right-hand side as in the following fictitious definition:
   18.12 -%
   18.13  \begin{isabelle}%
   18.14  \ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ \isadigit{1}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}%
   18.15 -\end{isabelle}%
   18.16 -
   18.17 +\end{isabelle}
   18.18  where \isa{dvd} means ``divides''.
   18.19  Isabelle rejects this ``definition'' because of the extra \isa{m} on the
   18.20  right-hand side, which would introduce an inconsistency (why?). What you
   18.21  should have written is
   18.22 -%
   18.23  \begin{isabelle}%
   18.24  \ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ \isadigit{1}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}%
   18.25 -\end{isabelle}%
   18.26 -
   18.27 +\end{isabelle}
   18.28  \end{warn}%
   18.29  \end{isamarkuptext}%
   18.30  \end{isabellebody}%
    19.1 --- a/doc-src/TutorialI/Misc/document/simp.tex	Mon Sep 11 17:59:53 2000 +0200
    19.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex	Mon Sep 11 18:00:47 2000 +0200
    19.3 @@ -0,0 +1,12 @@
    19.4 +%
    19.5 +\begin{isabellebody}%
    19.6 +\def\isabellecontext{simp}%
    19.7 +\isanewline
    19.8 +\isacommand{theory}\ simp\ {\isacharequal}\ Main{\isacharcolon}\isanewline
    19.9 +\isanewline
   19.10 +\isacommand{end}\isanewline
   19.11 +\end{isabellebody}%
   19.12 +%%% Local Variables:
   19.13 +%%% mode: latex
   19.14 +%%% TeX-master: "root"
   19.15 +%%% End:
    20.1 --- a/doc-src/TutorialI/Misc/document/types.tex	Mon Sep 11 17:59:53 2000 +0200
    20.2 +++ b/doc-src/TutorialI/Misc/document/types.tex	Mon Sep 11 18:00:47 2000 +0200
    20.3 @@ -1,5 +1,6 @@
    20.4  %
    20.5  \begin{isabellebody}%
    20.6 +\def\isabellecontext{types}%
    20.7  \isacommand{types}\ number\ \ \ \ \ \ \ {\isacharequal}\ nat\isanewline
    20.8  \ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
    20.9  \ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}%
    21.1 --- a/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Sep 11 17:59:53 2000 +0200
    21.2 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Sep 11 18:00:47 2000 +0200
    21.3 @@ -1,5 +1,6 @@
    21.4  %
    21.5  \begin{isabellebody}%
    21.6 +\def\isabellecontext{Induction}%
    21.7  %
    21.8  \begin{isamarkuptext}%
    21.9  Assuming we have defined our function such that Isabelle could prove
    22.1 --- a/doc-src/TutorialI/Recdef/document/Nested0.tex	Mon Sep 11 17:59:53 2000 +0200
    22.2 +++ b/doc-src/TutorialI/Recdef/document/Nested0.tex	Mon Sep 11 18:00:47 2000 +0200
    22.3 @@ -1,5 +1,6 @@
    22.4  %
    22.5  \begin{isabellebody}%
    22.6 +\def\isabellecontext{Nested0}%
    22.7  %
    22.8  \begin{isamarkuptext}%
    22.9  In \S\ref{sec:nested-datatype} we defined the datatype of terms%
    23.1 --- a/doc-src/TutorialI/Recdef/document/Nested1.tex	Mon Sep 11 17:59:53 2000 +0200
    23.2 +++ b/doc-src/TutorialI/Recdef/document/Nested1.tex	Mon Sep 11 18:00:47 2000 +0200
    23.3 @@ -1,5 +1,6 @@
    23.4  %
    23.5  \begin{isabellebody}%
    23.6 +\def\isabellecontext{Nested1}%
    23.7  \isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}%
    23.8  \begin{isamarkuptext}%
    23.9  \noindent
   23.10 @@ -20,11 +21,9 @@
   23.11  Remember that function \isa{size} is defined for each \isacommand{datatype}.
   23.12  However, the definition does not succeed. Isabelle complains about an
   23.13  unproved termination condition
   23.14 -%
   23.15  \begin{isabelle}%
   23.16  \ \ \ \ \ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}%
   23.17 -\end{isabelle}%
   23.18 -
   23.19 +\end{isabelle}
   23.20  where \isa{set} returns the set of elements of a list (no special
   23.21  knowledge of sets is required in the following) and \isa{term{\isacharunderscore}list{\isacharunderscore}size\ {\isacharcolon}{\isacharcolon}\ term\ list\ {\isasymRightarrow}\ nat} is an auxiliary function automatically defined by Isabelle
   23.22  (when \isa{term} was defined).  First we have to understand why the
    24.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Sep 11 17:59:53 2000 +0200
    24.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Sep 11 18:00:47 2000 +0200
    24.3 @@ -1,5 +1,6 @@
    24.4  %
    24.5  \begin{isabellebody}%
    24.6 +\def\isabellecontext{Nested2}%
    24.7  %
    24.8  \begin{isamarkuptext}%
    24.9  \noindent
   24.10 @@ -22,12 +23,10 @@
   24.11  \begin{isamarkuptxt}%
   24.12  \noindent
   24.13  This leaves us with a trivial base case \isa{trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ x} and the step case
   24.14 -%
   24.15  \begin{isabelle}%
   24.16  \ \ \ \ \ {\isasymforall}t{\isachardot}\ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t\ {\isasymLongrightarrow}\isanewline
   24.17  \ \ \ \ \ trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts%
   24.18 -\end{isabelle}%
   24.19 -
   24.20 +\end{isabelle}
   24.21  both of which are solved by simplification:%
   24.22  \end{isamarkuptxt}%
   24.23  \isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}{\isacharparenright}%
   24.24 @@ -62,12 +61,10 @@
   24.25  \isacommand{recdef} would try to prove the unprovable \isa{size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}}, without any assumption about \isa{t}.  Therefore
   24.26  \isacommand{recdef} has been supplied with the congruence theorem
   24.27  \isa{map{\isacharunderscore}cong}:
   24.28 -%
   24.29  \begin{isabelle}%
   24.30  \ \ \ \ \ {\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline
   24.31  \ \ \ \ \ {\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys%
   24.32 -\end{isabelle}%
   24.33 -
   24.34 +\end{isabelle}
   24.35  Its second premise expresses (indirectly) that the second argument of
   24.36  \isa{map} is only applied to elements of its third argument. Congruence
   24.37  rules for other higher-order functions on lists would look very similar but
    25.1 --- a/doc-src/TutorialI/Recdef/document/examples.tex	Mon Sep 11 17:59:53 2000 +0200
    25.2 +++ b/doc-src/TutorialI/Recdef/document/examples.tex	Mon Sep 11 18:00:47 2000 +0200
    25.3 @@ -1,5 +1,6 @@
    25.4  %
    25.5  \begin{isabellebody}%
    25.6 +\def\isabellecontext{examples}%
    25.7  %
    25.8  \begin{isamarkuptext}%
    25.9  Here is a simple example, the Fibonacci function:%
    26.1 --- a/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Sep 11 17:59:53 2000 +0200
    26.2 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Sep 11 18:00:47 2000 +0200
    26.3 @@ -1,5 +1,6 @@
    26.4  %
    26.5  \begin{isabellebody}%
    26.6 +\def\isabellecontext{simplification}%
    26.7  %
    26.8  \begin{isamarkuptext}%
    26.9  Once we have succeeded in proving all termination conditions, the recursion
   26.10 @@ -16,11 +17,9 @@
   26.11  \noindent
   26.12  According to the measure function, the second argument should decrease with
   26.13  each recursive call. The resulting termination condition
   26.14 -%
   26.15  \begin{isabelle}%
   26.16  \ \ \ \ \ n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n%
   26.17 -\end{isabelle}%
   26.18 -
   26.19 +\end{isabelle}
   26.20  is provded automatically because it is already present as a lemma in the
   26.21  arithmetic library. Thus the recursion equation becomes a simplification
   26.22  rule. Of course the equation is nonterminating if we are allowed to unfold
   26.23 @@ -29,23 +28,17 @@
   26.24  something else which leads to the same problem: it splits \isa{if}s if the
   26.25  condition simplifies to neither \isa{True} nor \isa{False}. For
   26.26  example, simplification reduces
   26.27 -%
   26.28  \begin{isabelle}%
   26.29  \ \ \ \ \ gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k%
   26.30 -\end{isabelle}%
   26.31 -
   26.32 +\end{isabelle}
   26.33  in one step to
   26.34 -%
   26.35  \begin{isabelle}%
   26.36  \ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ \isadigit{0}\ then\ m\ else\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k%
   26.37 -\end{isabelle}%
   26.38 -
   26.39 +\end{isabelle}
   26.40  where the condition cannot be reduced further, and splitting leads to
   26.41 -%
   26.42  \begin{isabelle}%
   26.43  \ \ \ \ \ {\isacharparenleft}n\ {\isacharequal}\ \isadigit{0}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymlongrightarrow}\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}%
   26.44 -\end{isabelle}%
   26.45 -
   26.46 +\end{isabelle}
   26.47  Since the recursive call \isa{gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}} is no longer protected by
   26.48  an \isa{if}, it is unfolded again, which leads to an infinite chain of
   26.49  simplification steps. Fortunately, this problem can be avoided in many
    27.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex	Mon Sep 11 17:59:53 2000 +0200
    27.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex	Mon Sep 11 18:00:47 2000 +0200
    27.3 @@ -1,5 +1,6 @@
    27.4  %
    27.5  \begin{isabellebody}%
    27.6 +\def\isabellecontext{termination}%
    27.7  %
    27.8  \begin{isamarkuptext}%
    27.9  When a function is defined via \isacommand{recdef}, Isabelle tries to prove
    28.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Sep 11 17:59:53 2000 +0200
    28.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Sep 11 18:00:47 2000 +0200
    28.3 @@ -1,5 +1,6 @@
    28.4  %
    28.5  \begin{isabellebody}%
    28.6 +\def\isabellecontext{ToyList}%
    28.7  \isacommand{theory}\ ToyList\ {\isacharequal}\ PreList{\isacharcolon}%
    28.8  \begin{isamarkuptext}%
    28.9  \noindent
    29.1 --- a/doc-src/TutorialI/Trie/document/Option2.tex	Mon Sep 11 17:59:53 2000 +0200
    29.2 +++ b/doc-src/TutorialI/Trie/document/Option2.tex	Mon Sep 11 18:00:47 2000 +0200
    29.3 @@ -1,5 +1,6 @@
    29.4  %
    29.5  \begin{isabellebody}%
    29.6 +\def\isabellecontext{Option2}%
    29.7  \isanewline
    29.8  \isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabellebody}%
    29.9  %%% Local Variables:
    30.1 --- a/doc-src/TutorialI/Trie/document/Trie.tex	Mon Sep 11 17:59:53 2000 +0200
    30.2 +++ b/doc-src/TutorialI/Trie/document/Trie.tex	Mon Sep 11 18:00:47 2000 +0200
    30.3 @@ -1,5 +1,6 @@
    30.4  %
    30.5  \begin{isabellebody}%
    30.6 +\def\isabellecontext{Trie}%
    30.7  %
    30.8  \begin{isamarkuptext}%
    30.9  To minimize running time, each node of a trie should contain an array that maps
    31.1 --- a/doc-src/TutorialI/isabelle.sty	Mon Sep 11 17:59:53 2000 +0200
    31.2 +++ b/doc-src/TutorialI/isabelle.sty	Mon Sep 11 18:00:47 2000 +0200
    31.3 @@ -6,10 +6,12 @@
    31.4  %% macros for Isabelle generated LaTeX output
    31.5  %%
    31.6  
    31.7 -%%% Simple document preparation (based on theory token language)
    31.8 +%%% Simple document preparation (based on theory token language and symbols)
    31.9  
   31.10  % isabelle environments
   31.11  
   31.12 +\newcommand{\isabellecontext}{UNKNOWN}
   31.13 +
   31.14  \newcommand{\isastyle}{\small\tt\slshape}
   31.15  \newcommand{\isastyleminor}{\small\tt\slshape}
   31.16  \newcommand{\isastyletext}{\normalsize\rm}