
diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Recdef/document/termination.tex
--- a/doc-src/TutorialI/Recdef/document/termination.tex	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Tue Apr 25 08:09:10 2000 +0200
@@ -4,8 +4,8 @@
 When a function is defined via \isacommand{recdef}, Isabelle tries to prove
 its termination with the help of the user-supplied measure.  All of the above
 examples are simple enough that Isabelle can prove automatically that the
-measure of the argument goes down in each recursive call. In that case
-$f$.\isa{simps} contains the defining equations (or variants derived from
+measure of the argument goes down in each recursive call. As a result,
+\isa{$f$.simps} will contain the defining equations (or variants derived from
 them) as theorems. For example, look (via \isacommand{thm}) at
 \isa{sep.simps} and \isa{sep1.simps} to see that they define the same
 function. What is more, those equations are automatically declared as
@@ -34,8 +34,8 @@
 \isacommand{apply}(arith)\isacommand{.}%
 \begin{isamarkuptext}%
 \noindent
-Because \isacommand{recdef}'s the termination prover involves simplification,
-we have declared our lemma a simplification rule. Therefore our second
+Because \isacommand{recdef}'s termination prover involves simplification,
+we have turned our lemma into a simplification rule. Therefore our second
 attempt to define our function will automatically take it into account:%
 \end{isamarkuptext}%
 \isacommand{consts}~g~::~{"}nat*nat~{\isasymRightarrow}~nat{"}\isanewline




