--- 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}%