diff -r d2a2c479b3cb -r e28870d8b223 doc-src/TutorialI/Recdef/Nested2.thy
--- a/doc-src/TutorialI/Recdef/Nested2.thy	Thu Dec 13 17:44:56 2001 +0100
+++ b/doc-src/TutorialI/Recdef/Nested2.thy	Thu Dec 13 17:57:55 2001 +0100
@@ -2,8 +2,6 @@
 theory Nested2 = Nested0:
 (*>*)
 
-text{*The termination condition is easily proved by induction:*}
-
 lemma [simp]: "t \<in> set ts \<longrightarrow> size t < Suc(term_list_size ts)"
 by(induct_tac ts, auto)
 (*<*)