# HG changeset patch
# User nipkow
# Date 1008262675 -3600
# Node ID e28870d8b223181219bd9608f8b16c56bc0b6e80
# Parent  d2a2c479b3cb639a4bde78b1f5f5a11334e99118
*** empty log message ***

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:
 *}
 
 (*<*)
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)
 (*<*)
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%
diff -r d2a2c479b3cb -r e28870d8b223 doc-src/TutorialI/Recdef/document/Nested2.tex
--- 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%