diff -r ac8ca15c556c -r 885e053ae664 doc-src/TutorialI/Recdef/document/simplification.tex
--- a/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Oct 08 12:13:34 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Oct 08 12:13:56 2001 +0200
@@ -19,7 +19,7 @@
 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%
+\ \ \ \ \ n\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n%
 \end{isabelle}
 is proved automatically because it is already present as a lemma in
 HOL\@.  Thus the recursion equation becomes a simplification
@@ -63,7 +63,7 @@
 \begin{isamarkuptext}%
 \noindent
 The order of equations is important: it hides the side condition
-\isa{n\ {\isasymnoteq}\ {\isadigit{0}}}.  Unfortunately, in general the case distinction
+\isa{n\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}}.  Unfortunately, in general the case distinction
 may not be expressible by pattern matching.
 
 A simple alternative is to replace \isa{if} by \isa{case},