--- a/doc-src/TutorialI/Recdef/document/termination.tex Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/termination.tex Wed Jan 24 12:29:10 2001 +0100
@@ -30,7 +30,7 @@
\isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
-It was not proved automatically because of the special nature of \isa{{\isacharminus}}
+It was not proved automatically because of the special nature of subtraction
on \isa{nat}. This requires more arithmetic than is tried by default:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline