--- 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},