--- a/doc-src/TutorialI/Recdef/document/termination.tex Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/termination.tex Fri Jan 05 18:32:57 2001 +0100
@@ -13,8 +13,8 @@
the same function. What is more, those equations are automatically declared as
simplification rules.
-In general, Isabelle may not be able to prove all termination conditions
-(there is one for each recursive call) automatically. For example,
+Isabelle may fail to prove some termination conditions
+(there is one for each recursive call). For example,
termination of the following artificial function%
\end{isamarkuptext}%
\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
@@ -22,8 +22,8 @@
\ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-is not proved automatically (although maybe it should be). Isabelle prints a
-kind of error message showing you what it was unable to prove. You will then
+is not proved automatically. Isabelle prints a
+message showing you what it was unable to prove. You will then
have to prove it as a separate lemma before you attempt the definition
of your function once more. In our case the required lemma is the obvious one:%
\end{isamarkuptext}%