diff -r d2a2c479b3cb -r e28870d8b223 doc-src/TutorialI/Recdef/Nested1.thy
--- a/doc-src/TutorialI/Recdef/Nested1.thy	Thu Dec 13 17:44:56 2001 +0100
+++ b/doc-src/TutorialI/Recdef/Nested1.thy	Thu Dec 13 17:57:55 2001 +0100
@@ -34,6 +34,8 @@
 which equals @{term"Suc(term_list_size ts)"}.  We will now prove the termination condition and
 continue with our definition.  Below we return to the question of how
 \isacommand{recdef} knows about @{term map}.
+
+The termination condition is easily proved by induction:
 *}
 
 (*<*)