--- 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: