--- a/doc-src/TutorialI/Recdef/document/simplification.tex Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex Wed Dec 12 09:04:20 2001 +0100
@@ -23,7 +23,7 @@
According to the measure function, the second argument should decrease with
each recursive call. The resulting termination condition
\begin{isabelle}%
-\ \ \ \ \ n\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n%
+\ \ \ \ \ n\ {\isasymnoteq}\ {\isadigit{0}}\ {\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
@@ -70,7 +70,7 @@
\begin{isamarkuptext}%
\noindent
The order of equations is important: it hides the side condition
-\isa{n\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}}. Unfortunately, in general the case distinction
+\isa{n\ {\isasymnoteq}\ {\isadigit{0}}}. Unfortunately, in general the case distinction
may not be expressible by pattern matching.
A simple alternative is to replace \isa{if} by \isa{case},