--- a/doc-src/TutorialI/Recdef/termination.thy Fri May 18 16:45:55 2001 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy Fri May 18 17:18:43 2001 +0200
@@ -3,10 +3,10 @@
(*>*)
text{*
-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$@{text".simps"} will contain the defining equations (or variants derived
from them) as theorems. For example, look (via \isacommand{thm}) at
@{thm[source]sep.simps} and @{thm[source]sep1.simps} to see that they define