1.1 --- a/doc-src/TutorialI/Recdef/termination.thy Sun Nov 26 11:37:49 2000 +0100
1.2 +++ b/doc-src/TutorialI/Recdef/termination.thy Mon Nov 27 10:38:43 2000 +0100
1.3 @@ -13,7 +13,7 @@
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 condition
1.8 +In general, Isabelle may not be able to prove all termination conditions
1.9 (there is one for each recursive call) automatically. For example,
1.10 termination of the following artificial function
1.11 *}