
diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Recdef/document/Nested2.tex
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Tue Dec 17 11:05:41 2002 +0100
@@ -2,6 +2,7 @@
 \begin{isabellebody}%
 \def\isabellecontext{Nested{\isadigit{2}}}%
 \isanewline
+\isanewline
 \isamarkupfalse%
 \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%
@@ -78,6 +79,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%
+\isanewline
 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -97,6 +99,7 @@
 %recdef from generating sensible termination conditions.%
 \end{isamarkuptext}%
 \isamarkuptrue%
+\isanewline
 \isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables:




