diff -r 06206298e4d0 -r ed3964d1f1a4 doc-src/TutorialI/Recdef/document/termination.tex --- a/doc-src/TutorialI/Recdef/document/termination.tex Sun Nov 26 11:37:49 2000 +0100 +++ b/doc-src/TutorialI/Recdef/document/termination.tex Mon Nov 27 10:38:43 2000 +0100 @@ -13,7 +13,7 @@ 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 condition +In general, Isabelle may not be able to prove all termination conditions (there is one for each recursive call) automatically. For example, termination of the following artificial function% \end{isamarkuptext}%