diff -r d2a2c479b3cb -r e28870d8b223 doc-src/TutorialI/Recdef/document/Nested1.tex
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex	Thu Dec 13 17:44:56 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex	Thu Dec 13 17:57:55 2001 +0100
@@ -38,7 +38,9 @@
 recursive call of \isa{trev} is strictly less than \isa{size\ {\isacharparenleft}App\ f\ ts{\isacharparenright}},
 which equals \isa{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}.%
+\isacommand{recdef} knows about \isa{map}.
+
+The termination condition is easily proved by induction:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%