--- a/doc-src/TutorialI/Recdef/document/examples.tex Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/examples.tex Tue Apr 25 08:09:10 2000 +0200
@@ -11,7 +11,7 @@
\begin{isamarkuptext}%
\noindent
The definition of \isa{fib} is accompanied by a \bfindex{measure function}
-\isa{\isasymlambda{}n.$\;$n} that maps the argument of \isa{fib} to a
+\isa{\isasymlambda{}n.$\;$n} which maps the argument of \isa{fib} to a
natural number. The requirement is that in each equation the measure of the
argument on the left-hand side is strictly greater than the measure of the
argument of each recursive call. In the case of \isa{fib} this is
@@ -74,7 +74,7 @@
~~{"}swap12~zs~~~~~~~=~zs{"}%
\begin{isamarkuptext}%
\noindent
-In the non-recursive case the termination measure degenerates to the empty
+For non-recursive functions the termination measure degenerates to the empty
set \isa{\{\}}.%
\end{isamarkuptext}%
\end{isabelle}%