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