--- a/doc-src/TutorialI/Recdef/Nested1.thy Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy Tue Sep 12 15:43:15 2000 +0200
@@ -23,9 +23,9 @@
However, the definition does not succeed. Isabelle complains about an
unproved termination condition
@{term[display]"t : set ts --> size t < Suc (term_list_size ts)"}
-where @{term"set"} returns the set of elements of a list (no special
-knowledge of sets is required in the following) and @{text"term_list_size ::
-term list \<Rightarrow> nat"} is an auxiliary function automatically defined by Isabelle
+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
recursive call of @{term"trev"} underneath @{term"map"} leads to the above
condition. The reason is that \isacommand{recdef} ``knows'' that @{term"map"}