--- a/doc-src/TutorialI/Recdef/Nested1.thy Fri Jan 12 16:28:14 2001 +0100
+++ b/doc-src/TutorialI/Recdef/Nested1.thy Fri Jan 12 16:32:01 2001 +0100
@@ -4,7 +4,7 @@
text{*\noindent
Although the definition of @{term trev} is quite natural, we will have
-overcome a minor difficulty in convincing Isabelle of is termination.
+to overcome a minor difficulty in convincing Isabelle of its termination.
It is precisely this difficulty that is the \textit{raison d'\^etre} of
this subsection.
@@ -25,13 +25,13 @@
where @{term set} returns the set of elements of a list
and @{text"term_list_size :: term list \<Rightarrow> nat"} is an auxiliary
function automatically defined by Isabelle
-(when @{text term} was defined). First we have to understand why the
+(while processing the declaration of @{text term}). First we have to understand why the
recursive call of @{term trev} underneath @{term map} leads to the above
condition. The reason is that \isacommand{recdef} ``knows'' that @{term map}
-will apply @{term trev} only to elements of @{term ts}. Thus the above
+will apply @{term trev} only to elements of @{term ts}. Thus the
condition expresses that the size of the argument @{prop"t : set ts"} of any
-recursive call of @{term trev} is strictly less than @{prop"size(App f ts) =
-Suc(term_list_size ts)"}. We will now prove the termination condition and
+recursive call of @{term trev} is strictly less than @{term"size(App f ts)"},
+which equals @{term"Suc(term_list_size ts)"}. We will now prove the termination condition and
continue with our definition. Below we return to the question of how
\isacommand{recdef} ``knows'' about @{term map}.
*};