diff -r 5b6305cab436 -r 9feb1e0c4cb3 doc-src/TutorialI/Recdef/document/Nested1.tex
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex	Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex	Tue Sep 12 15:43:15 2000 +0200
@@ -24,8 +24,9 @@
 \begin{isabelle}%
 \ \ \ \ \ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}%
 \end{isabelle}
-where \isa{set} returns the set of elements of a list (no special
-knowledge of sets is required in the following) and \isa{term{\isacharunderscore}list{\isacharunderscore}size\ {\isacharcolon}{\isacharcolon}\ term\ list\ {\isasymRightarrow}\ nat} is an auxiliary function automatically defined by Isabelle
+where \isa{set} returns the set of elements of a list
+and \isa{term{\isacharunderscore}list{\isacharunderscore}size\ {\isacharcolon}{\isacharcolon}\ term\ list\ {\isasymRightarrow}\ nat} is an auxiliary
+function automatically defined by Isabelle
 (when \isa{term} was defined).  First we have to understand why the
 recursive call of \isa{trev} underneath \isa{map} leads to the above
 condition. The reason is that \isacommand{recdef} ``knows'' that \isa{map}