--- 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}