diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Tue Dec 17 11:05:41 2002 +0100
@@ -217,6 +217,7 @@
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \isamarkupfalse%
+\isanewline
 \isamarkupfalse%
 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
@@ -340,6 +341,7 @@
 Let us simplify a case analysis over lists:\index{*list.split (theorem)}%
 \end{isamarkuptxt}%
 \isamarkuptrue%
+\isanewline
 \isamarkupfalse%
 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline
 \isamarkupfalse%
@@ -360,6 +362,7 @@
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \isamarkupfalse%
+\isanewline
 \isamarkupfalse%
 \isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
@@ -381,6 +384,7 @@
 either locally%
 \end{isamarkuptext}%
 \isamarkuptrue%
+\isanewline
 \isamarkupfalse%
 \isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
@@ -489,6 +493,7 @@
 \isamarkuptrue%
 \isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
 \isamarkupfalse%
+\isanewline
 \isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables: