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