doc-src/TutorialI/Recdef/termination.thy
changeset 10522 ed3964d1f1a4
parent 10186 499637e8f2c6
child 10654 458068404143
     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  *}