--- a/doc-src/TutorialI/Recdef/Nested1.thy Fri Sep 01 18:29:52 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy Fri Sep 01 19:09:44 2000 +0200
@@ -26,9 +26,9 @@
@{term[display]"t : set ts --> size t < Suc (term_list_size ts)"}
\end{quote}
where @{term"set"} returns the set of elements of a list (no special
-knowledge of sets is required in the following) and @{name"term_list_size ::
+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
-(when @{name"term"} was defined). First we have to understand why the
+(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"}
will apply @{term"trev"} only to elements of @{term"ts"}. Thus the above