# HG changeset patch
# User wenzelm
# Date 968688047 -7200
# Node ID 3370f6aa32001e2775b8acce58e799c30d954447
# Parent  fe13743ffc8b352764e61a4b185092d183d98260
updated;

diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/CodeGen/document/CodeGen.tex
--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{CodeGen}%
 %
 \isamarkupsection{Case study: compiling expressions}
 %
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Datatype/document/ABexpr.tex
--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{ABexpr}%
 %
 \begin{isamarkuptext}%
 Sometimes it is necessary to define two datatypes that depend on each
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Datatype/document/Fundata.tex
--- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{Fundata}%
 \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}%
 \begin{isamarkuptext}%
 \noindent
@@ -10,11 +11,9 @@
 \isa{nat}, we have an infinitely branching tree because each node
 has as many subtrees as there are natural numbers. How can we possibly
 write down such a tree? Using functional notation! For example, the term
-%
 \begin{isabelle}%
 \ \ \ \ \ Branch\ \isadigit{0}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Branch\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
-\end{isabelle}%
-
+\end{isabelle}
 of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose
 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
 has merely \isa{Tip}s as further subtrees.
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Datatype/document/Nested.tex
--- a/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{Nested}%
 %
 \begin{isamarkuptext}%
 So far, all datatypes had the property that on the right-hand side of their
@@ -71,11 +72,9 @@
 \begin{exercise}
 The fact that substitution distributes over composition can be expressed
 roughly as follows:
-%
 \begin{isabelle}%
 \ \ \ \ \ subst\ {\isacharparenleft}f\ o\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}%
-\end{isabelle}%
-
+\end{isabelle}
 Correct this statement (you will find that it does not type-check),
 strengthen it, and prove it. (Note: \isaindexbold{o} is function composition;
 its definition is found in theorem \isa{o{\isacharunderscore}def}).
@@ -89,11 +88,9 @@
 The experienced functional programmer may feel that our above definition of
 \isa{subst} is unnecessarily complicated in that \isa{substs} is
 completely unnecessary. The \isa{App}-case can be defined directly as
-%
 \begin{isabelle}%
 \ \ \ \ \ subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}%
-\end{isabelle}%
-
+\end{isabelle}
 where \isa{map} is the standard list function such that
 \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
 insists on the above fixed format. Fortunately, we can easily \emph{prove}
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Datatype/document/unfoldnested.tex
--- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{unfoldnested}%
 \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
 \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}%
 %%% Local Variables:
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{Ifexpr}%
 %
 \begin{isamarkuptext}%
 \subsubsection{How can we model boolean expressions?}
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{AdvancedInd}%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -85,16 +86,16 @@
 \begin{isamarkuptext}%
 \noindent
 or the wholesale stripping of \isa{{\isasymforall}} and
-\isa{{\isasymlongrightarrow}} in the conclusion via \isa{rulify}%
+\isa{{\isasymlongrightarrow}} in the conclusion via \isa{rulified}%
 \end{isamarkuptext}%
-\isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}rulify{\isacharbrackright}%
+\isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}rulified{\isacharbrackright}%
 \begin{isamarkuptext}%
 \noindent
 yielding \isa{{\isasymlbrakk}A\ y{\isacharsemicolon}\ B\ y{\isasymrbrakk}\ {\isasymLongrightarrow}\ B\ y\ {\isasymand}\ A\ y}.
 You can go one step further and include these derivations already in the
 statement of your original lemma, thus avoiding the intermediate step:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ myrule{\isacharbrackleft}rulify{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}%
+\isacommand{lemma}\ myrule{\isacharbrackleft}rulified{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}%
 \begin{isamarkuptext}%
 \bigskip
 
@@ -119,12 +120,10 @@
 Structural induction on \isa{nat} is
 usually known as ``mathematical induction''. There is also ``complete
 induction'', where you must prove $P(n)$ under the assumption that $P(m)$
-holds for all $m<n$. In Isabelle, this is the theorem \isa{less{\isacharunderscore}induct}:
-%
+holds for all $m<n$. In Isabelle, this is the theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}:
 \begin{isabelle}%
 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
-\end{isabelle}%
-
+\end{isabelle}
 Here is an example of its application.%
 \end{isamarkuptext}%
 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isacharequal}{\isachargreater}\ nat{\isachardoublequote}\isanewline
@@ -142,11 +141,11 @@
 \isacommand{lemma}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
-To perform induction on \isa{k} using \isa{less{\isacharunderscore}induct}, we use the same
+To perform induction on \isa{k} using \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}, we use the same
 general induction method as for recursion induction (see
 \S\ref{sec:recdef-induction}):%
 \end{isamarkuptxt}%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ k\ rule{\isacharcolon}less{\isacharunderscore}induct{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ k\ rule{\isacharcolon}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
 which leaves us with the following proof state:
@@ -163,7 +162,7 @@
 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
 \end{isabelle}%
 \end{isamarkuptxt}%
-\isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}%
+\isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 It is not surprising if you find the last step puzzling.
@@ -186,13 +185,13 @@
 
 We can now derive the desired \isa{i\ {\isasymle}\ f\ i} from \isa{f{\isacharunderscore}incr}:%
 \end{isamarkuptext}%
-\isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rulify{\isacharcomma}\ OF\ refl{\isacharbrackright}%
+\isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rulified{\isacharcomma}\ OF\ refl{\isacharbrackright}%
 \begin{isamarkuptext}%
 \noindent
 The final \isa{refl} gets rid of the premise \isa{{\isacharquery}k\ {\isacharequal}\ f\ {\isacharquery}i}. Again,
 we could have included this derivation in the original statement of the lemma:%
 \end{isamarkuptext}%
-\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}%
+\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}%
 \begin{isamarkuptext}%
 \begin{exercise}
 From the above axiom and lemma for \isa{f} show that \isa{f} is the
@@ -220,7 +219,7 @@
 \label{sec:derive-ind}
 Induction schemas are ordinary theorems and you can derive new ones
 whenever you wish.  This section shows you how to, using the example
-of \isa{less{\isacharunderscore}induct}. Assume we only have structural induction
+of \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}. Assume we only have structural induction
 available for \isa{nat} and want to derive complete induction. This
 requires us to generalize the statement first:%
 \end{isamarkuptext}%
@@ -240,32 +239,28 @@
 \begin{isamarkuptext}%
 \noindent
 The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction:
-%
 \begin{isabelle}%
 \ \ \ \ \ {\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
-\end{isabelle}%
-
+\end{isabelle}
 
 Now it is straightforward to derive the original version of
-\isa{less{\isacharunderscore}induct} by manipulting the conclusion of the above lemma:
+\isa{nat{\isacharunderscore}less{\isacharunderscore}induct} by manipulting the conclusion of the above lemma:
 instantiate \isa{n} by \isa{Suc\ n} and \isa{m} by \isa{n} and
 remove the trivial condition \isa{n\ {\isacharless}\ Sc\ n}. Fortunately, this
 happens automatically when we add the lemma as a new premise to the
 desired goal:%
 \end{isamarkuptext}%
-\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
+\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
 \isacommand{by}{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 Finally we should mention that HOL already provides the mother of all
 inductions, \emph{wellfounded induction} (\isa{wf{\isacharunderscore}induct}):
-%
 \begin{isabelle}%
 \ \ \ \ \ {\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%
-\end{isabelle}%
-
+\end{isabelle}
 where \isa{wf\ r} means that the relation \isa{r} is wellfounded.
-For example \isa{less{\isacharunderscore}induct} is the special case where \isa{r} is
+For example \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} is the special case where \isa{r} is
 \isa{{\isacharless}} on \isa{nat}. For details see the library.%
 \end{isamarkuptext}%
 \end{isabellebody}%
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Misc/document/Itrev.tex
--- a/doc-src/TutorialI/Misc/document/Itrev.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{Itrev}%
 %
 \isamarkupsection{Induction heuristics}
 %
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Misc/document/Tree.tex
--- a/doc-src/TutorialI/Misc/document/Tree.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{Tree}%
 %
 \begin{isamarkuptext}%
 \noindent
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Misc/document/Tree2.tex
--- a/doc-src/TutorialI/Misc/document/Tree2.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree2.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{Tree2}%
 %
 \begin{isamarkuptext}%
 \noindent In Exercise~\ref{ex:Tree} we defined a function
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Misc/document/arith1.tex
--- a/doc-src/TutorialI/Misc/document/arith1.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith1.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{arith1}%
 \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
 \end{isabellebody}%
 %%% Local Variables:
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Misc/document/arith2.tex
--- a/doc-src/TutorialI/Misc/document/arith2.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith2.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{arith2}%
 \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
 \isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline
 \end{isabellebody}%
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Misc/document/arith3.tex
--- a/doc-src/TutorialI/Misc/document/arith3.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith3.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{arith3}%
 \isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}\isadigit{0}\ {\isasymor}\ n{\isacharequal}\isadigit{1}{\isachardoublequote}\isanewline
 \end{isabellebody}%
 %%% Local Variables:
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Misc/document/case_exprs.tex
--- a/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{case_exprs}%
 %
 \isamarkupsubsection{Case expressions}
 %
@@ -7,11 +8,9 @@
 \label{sec:case-expressions}
 HOL also features \isaindexbold{case}-expressions for analyzing
 elements of a datatype. For example,
-%
 \begin{isabelle}%
 \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y%
-\end{isabelle}%
-
+\end{isabelle}
 evaluates to \isa{\isadigit{1}} if \isa{xs} is \isa{{\isacharbrackleft}{\isacharbrackright}} and to \isa{y} if 
 \isa{xs} is \isa{y\ {\isacharhash}\ ys}. (Since the result in both branches must be of
 the same type, it follows that \isa{y} is of type \isa{nat} and hence
@@ -36,18 +35,14 @@
 \noindent
 Nested patterns can be simulated by nested \isa{case}-expressions: instead
 of
-%
 \begin{isabelle}%
 \ \ \ \ \ 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%
-\end{isabelle}%
-
+\end{isabelle}
 write
-%
 \begin{isabelle}%
 \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\isanewline
 \ \ \ \ \ {\isacharbar}\ x\ {\isacharhash}\ ys\ {\isasymRightarrow}\ case\ ys\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ x\ {\isacharbar}\ y\ {\isacharhash}\ zs\ {\isasymRightarrow}\ y%
-\end{isabelle}%
-
+\end{isabelle}
 
 Note that \isa{case}-expressions may need to be enclosed in parentheses to
 indicate their scope%
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Misc/document/fakenat.tex
--- a/doc-src/TutorialI/Misc/document/fakenat.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/fakenat.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{fakenat}%
 %
 \begin{isamarkuptext}%
 \noindent
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,14 +1,13 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{natsum}%
 %
 \begin{isamarkuptext}%
 \noindent
 In particular, there are \isa{case}-expressions, for example
-%
 \begin{isabelle}%
 \ \ \ \ \ case\ n\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m%
-\end{isabelle}%
-
+\end{isabelle}
 primitive recursion, for example%
 \end{isamarkuptext}%
 \isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Misc/document/pairs.tex
--- a/doc-src/TutorialI/Misc/document/pairs.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/pairs.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{pairs}%
 %
 \begin{isamarkuptext}%
 HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ *
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Misc/document/prime_def.tex
--- a/doc-src/TutorialI/Misc/document/prime_def.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/prime_def.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,24 +1,21 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{prime_def}%
 %
 \begin{isamarkuptext}%
 \begin{warn}
 A common mistake when writing definitions is to introduce extra free
 variables on the right-hand side as in the following fictitious definition:
-%
 \begin{isabelle}%
 \ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ \isadigit{1}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}%
-\end{isabelle}%
-
+\end{isabelle}
 where \isa{dvd} means ``divides''.
 Isabelle rejects this ``definition'' because of the extra \isa{m} on the
 right-hand side, which would introduce an inconsistency (why?). What you
 should have written is
-%
 \begin{isabelle}%
 \ \ \ \ \ {\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}%
-\end{isabelle}%
-
+\end{isabelle}
 \end{warn}%
 \end{isamarkuptext}%
 \end{isabellebody}%
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -0,0 +1,12 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{simp}%
+\isanewline
+\isacommand{theory}\ simp\ {\isacharequal}\ Main{\isacharcolon}\isanewline
+\isanewline
+\isacommand{end}\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Misc/document/types.tex
--- a/doc-src/TutorialI/Misc/document/types.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/types.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{types}%
 \isacommand{types}\ number\ \ \ \ \ \ \ {\isacharequal}\ nat\isanewline
 \ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
 \ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}%
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Recdef/document/Induction.tex
--- a/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{Induction}%
 %
 \begin{isamarkuptext}%
 Assuming we have defined our function such that Isabelle could prove
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Recdef/document/Nested0.tex
--- a/doc-src/TutorialI/Recdef/document/Nested0.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{Nested0}%
 %
 \begin{isamarkuptext}%
 In \S\ref{sec:nested-datatype} we defined the datatype of terms%
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Recdef/document/Nested1.tex
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{Nested1}%
 \isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
@@ -20,11 +21,9 @@
 Remember that function \isa{size} is defined for each \isacommand{datatype}.
 However, the definition does not succeed. Isabelle complains about an
 unproved termination condition
-%
 \begin{isabelle}%
 \ \ \ \ \ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}%
-\end{isabelle}%
-
+\end{isabelle}
 where \isa{set} returns the set of elements of a list (no special
 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
 (when \isa{term} was defined).  First we have to understand why the
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Recdef/document/Nested2.tex
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{Nested2}%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -22,12 +23,10 @@
 \begin{isamarkuptxt}%
 \noindent
 This leaves us with a trivial base case \isa{trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ x} and the step case
-%
 \begin{isabelle}%
 \ \ \ \ \ {\isasymforall}t{\isachardot}\ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t\ {\isasymLongrightarrow}\isanewline
 \ \ \ \ \ trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts%
-\end{isabelle}%
-
+\end{isabelle}
 both of which are solved by simplification:%
 \end{isamarkuptxt}%
 \isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}{\isacharparenright}%
@@ -62,12 +61,10 @@
 \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
 \isacommand{recdef} has been supplied with the congruence theorem
 \isa{map{\isacharunderscore}cong}:
-%
 \begin{isabelle}%
 \ \ \ \ \ {\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline
 \ \ \ \ \ {\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys%
-\end{isabelle}%
-
+\end{isabelle}
 Its second premise expresses (indirectly) that the second argument of
 \isa{map} is only applied to elements of its third argument. Congruence
 rules for other higher-order functions on lists would look very similar but
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Recdef/document/examples.tex
--- a/doc-src/TutorialI/Recdef/document/examples.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/examples.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{examples}%
 %
 \begin{isamarkuptext}%
 Here is a simple example, the Fibonacci function:%
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Recdef/document/simplification.tex
--- a/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{simplification}%
 %
 \begin{isamarkuptext}%
 Once we have succeeded in proving all termination conditions, the recursion
@@ -16,11 +17,9 @@
 \noindent
 According to the measure function, the second argument should decrease with
 each recursive call. The resulting termination condition
-%
 \begin{isabelle}%
 \ \ \ \ \ n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n%
-\end{isabelle}%
-
+\end{isabelle}
 is provded automatically because it is already present as a lemma in the
 arithmetic library. Thus the recursion equation becomes a simplification
 rule. Of course the equation is nonterminating if we are allowed to unfold
@@ -29,23 +28,17 @@
 something else which leads to the same problem: it splits \isa{if}s if the
 condition simplifies to neither \isa{True} nor \isa{False}. For
 example, simplification reduces
-%
 \begin{isabelle}%
 \ \ \ \ \ gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k%
-\end{isabelle}%
-
+\end{isabelle}
 in one step to
-%
 \begin{isabelle}%
 \ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ \isadigit{0}\ then\ m\ else\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k%
-\end{isabelle}%
-
+\end{isabelle}
 where the condition cannot be reduced further, and splitting leads to
-%
 \begin{isabelle}%
 \ \ \ \ \ {\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}%
-\end{isabelle}%
-
+\end{isabelle}
 Since the recursive call \isa{gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}} is no longer protected by
 an \isa{if}, it is unfolded again, which leads to an infinite chain of
 simplification steps. Fortunately, this problem can be avoided in many
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Recdef/document/termination.tex
--- a/doc-src/TutorialI/Recdef/document/termination.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{termination}%
 %
 \begin{isamarkuptext}%
 When a function is defined via \isacommand{recdef}, Isabelle tries to prove
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{ToyList}%
 \isacommand{theory}\ ToyList\ {\isacharequal}\ PreList{\isacharcolon}%
 \begin{isamarkuptext}%
 \noindent
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Trie/document/Option2.tex
--- a/doc-src/TutorialI/Trie/document/Option2.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Option2.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{Option2}%
 \isanewline
 \isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabellebody}%
 %%% Local Variables:
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Trie/document/Trie.tex
--- a/doc-src/TutorialI/Trie/document/Trie.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{Trie}%
 %
 \begin{isamarkuptext}%
 To minimize running time, each node of a trie should contain an array that maps
diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/isabelle.sty
--- a/doc-src/TutorialI/isabelle.sty	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/isabelle.sty	Mon Sep 11 18:00:47 2000 +0200
@@ -6,10 +6,12 @@
 %% macros for Isabelle generated LaTeX output
 %%
 
-%%% Simple document preparation (based on theory token language)
+%%% Simple document preparation (based on theory token language and symbols)
 
 % isabelle environments
 
+\newcommand{\isabellecontext}{UNKNOWN}
+
 \newcommand{\isastyle}{\small\tt\slshape}
 \newcommand{\isastyleminor}{\small\tt\slshape}
 \newcommand{\isastyletext}{\normalsize\rm}