--- a/doc-src/TutorialI/Misc/document/simp.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex Wed Jan 15 16:43:12 2003 +0100
@@ -217,9 +217,9 @@
\end{isamarkuptxt}%
\isamarkuptrue%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -293,7 +293,8 @@
the lemma below is proved by plain simplification:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -341,7 +342,6 @@
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%
@@ -362,9 +362,9 @@
\end{isamarkuptxt}%
\isamarkuptrue%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -384,9 +384,9 @@
either locally%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -454,7 +454,8 @@
\isamarkupfalse%
\isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -492,8 +493,8 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
+\isanewline
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables: