--- a/doc-src/TutorialI/Advanced/document/WFrec.tex Tue Feb 27 23:25:47 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Wed Feb 28 12:37:48 2001 +0100
@@ -90,7 +90,7 @@
\isacommand{apply}\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}%
\begin{isamarkuptxt}%
\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymlbrakk}y\ {\isacharless}\ x{\isacharsemicolon}\ x\ {\isasymle}\ N{\isasymrbrakk}\ {\isasymLongrightarrow}\ N\ {\isacharminus}\ x\ {\isacharless}\ N\ {\isacharminus}\ y%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ {\isasymlbrakk}b\ {\isacharless}\ a{\isacharsemicolon}\ a\ {\isasymle}\ N{\isasymrbrakk}\ {\isasymLongrightarrow}\ N\ {\isacharminus}\ a\ {\isacharless}\ N\ {\isacharminus}\ b%
\end{isabelle}
\noindent