1.1 --- a/doc-src/TutorialI/Recdef/termination.thy	Fri Jan 05 18:32:33 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Recdef/termination.thy	Fri Jan 05 18:32:57 2001 +0100
     1.3 @@ -13,8 +13,8 @@
     1.4  the same function. What is more, those equations are automatically declared as
     1.5  simplification rules.
     1.6  
     1.7 -In general, Isabelle may not be able to prove all termination conditions
     1.8 -(there is one for each recursive call) automatically. For example,
     1.9 +Isabelle may fail to prove some termination conditions
    1.10 +(there is one for each recursive call).  For example,
    1.11  termination of the following artificial function
    1.12  *}
    1.13  
    1.14 @@ -23,8 +23,8 @@
    1.15    "f(x,y) = (if x \<le> y then x else f(x,y+1))";
    1.16  
    1.17  text{*\noindent
    1.18 -is not proved automatically (although maybe it should be). Isabelle prints a
    1.19 -kind of error message showing you what it was unable to prove. You will then
    1.20 +is not proved automatically. Isabelle prints a
    1.21 +message showing you what it was unable to prove. You will then
    1.22  have to prove it as a separate lemma before you attempt the definition
    1.23  of your function once more. In our case the required lemma is the obvious one:
    1.24  *}