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: