diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Recdef/document/termination.tex
--- 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}%