doc-src/TutorialI/Recdef/document/termination.tex
changeset 10971 6852682eaf16
parent 10795 9e888d60d3e5
child 11309 d666f11ca2d4
     1.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex	Wed Jan 24 11:59:15 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex	Wed Jan 24 12:29:10 2001 +0100
     1.3 @@ -30,7 +30,7 @@
     1.4  \isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}%
     1.5  \begin{isamarkuptxt}%
     1.6  \noindent
     1.7 -It was not proved automatically because of the special nature of \isa{{\isacharminus}}
     1.8 +It was not proved automatically because of the special nature of subtraction
     1.9  on \isa{nat}. This requires more arithmetic than is tried by default:%
    1.10  \end{isamarkuptxt}%
    1.11  \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline