--- a/doc-src/TutorialI/Recdef/document/Nested1.tex Fri Sep 01 18:29:52 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Fri Sep 01 19:09:44 2000 +0200
@@ -23,7 +23,7 @@
\begin{quote}
\begin{isabelle}%
-\mbox{t}\ {\isasymin}\ set\ \mbox{ts}\ {\isasymlongrightarrow}\ size\ \mbox{t}\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}
+t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}
\end{isabelle}%
\end{quote}
@@ -32,9 +32,9 @@
(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}
-will apply \isa{trev} only to elements of \isa{\mbox{ts}}. Thus the above
-condition expresses that the size of the argument \isa{\mbox{t}\ {\isasymin}\ set\ \mbox{ts}} of any
-recursive call of \isa{trev} is strictly less than \isa{size\ {\isacharparenleft}App\ \mbox{f}\ \mbox{ts}{\isacharparenright}\ {\isacharequal}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}. We will now prove the termination condition and
+will apply \isa{trev} only to elements of \isa{ts}. Thus the above
+condition expresses that the size of the argument \isa{t\ {\isasymin}\ set\ ts} of any
+recursive call of \isa{trev} is strictly less than \isa{size\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}}. We will now prove the termination condition and
continue with our definition. Below we return to the question of how
\isacommand{recdef} ``knows'' about \isa{map}.%
\end{isamarkuptext}%