diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Misc/document/simp.tex
--- 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}%