diff -r b28bbb153603 -r d666f11ca2d4 doc-src/TutorialI/Recdef/document/termination.tex
--- a/doc-src/TutorialI/Recdef/document/termination.tex	Fri May 18 16:45:55 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Fri May 18 17:18:43 2001 +0200
@@ -3,10 +3,10 @@
 \def\isabellecontext{termination}%
 %
 \begin{isamarkuptext}%
-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. As a result,
+When a function~$f$ is defined via \isacommand{recdef}, Isabelle tries to prove
+its termination with the help of the user-supplied measure.  Each of the examples
+above is simple enough that Isabelle can automatically prove that the
+argument's measure decreases in each recursive call. As a result,
 $f$\isa{{\isachardot}simps} will contain the defining equations (or variants derived
 from them) as theorems. For example, look (via \isacommand{thm}) at
 \isa{sep{\isachardot}simps} and \isa{sep{\isadigit{1}}{\isachardot}simps} to see that they define