--- a/doc-src/TutorialI/Misc/document/simp.tex Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
%
\begin{isabellebody}%
\def\isabellecontext{simp}%
+\isamarkupfalse%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
-\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
@@ -261,7 +261,6 @@
can be proved by simplification. Thus we could have proved the lemma outright by%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
@@ -269,7 +268,6 @@
\isadelimproof
%
\endisadelimproof
-\isamarkupfalse%
%
\isadelimproof
%
@@ -277,8 +275,7 @@
%
\isatagproof
\isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
-%
+{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
@@ -390,7 +387,6 @@
\endisadelimproof
%
\isatagproof
-\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
@@ -450,7 +446,6 @@
Let us simplify a case analysis over lists:\index{*list.split (theorem)}%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
@@ -482,7 +477,6 @@
lemma above can be proved in one step by%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
@@ -490,7 +484,6 @@
\isadelimproof
%
\endisadelimproof
-\isamarkupfalse%
%
\isadelimproof
%
@@ -498,8 +491,7 @@
%
\isatagproof
\isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}\isamarkupfalse%
-%
+{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
@@ -524,7 +516,6 @@
either locally%
\end{isamarkuptext}%
\isamarkuptrue%
-\isamarkupfalse%
%
\isadelimproof
%
@@ -532,8 +523,7 @@
%
\isatagproof
\isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}\isamarkupfalse%
-%
+{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
@@ -594,7 +584,6 @@
\end{warn}%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
@@ -622,8 +611,7 @@
%
\isatagproof
\isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse%
-%
+{\isacharparenleft}simp{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
@@ -772,7 +760,6 @@
\endisadelimtheory
%
\isatagtheory
-\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%