--- 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:
*}
(*<*)
--- 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)
(*<*)
--- 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%
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex Thu Dec 13 17:44:56 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Thu Dec 13 17:57:55 2001 +0100
@@ -1,12 +1,8 @@
%
\begin{isabellebody}%
\def\isabellecontext{Nested{\isadigit{2}}}%
+\isanewline
\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-The termination condition is easily proved by induction:%
-\end{isamarkuptext}%
-\isamarkuptrue%
\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc{\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}\isamarkupfalse%