diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Types/document/Pairs.tex
--- a/doc-src/TutorialI/Types/document/Pairs.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Pairs.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Pairs}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -132,7 +132,6 @@
 simplification and splitting in one command that proves the goal outright:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -140,7 +139,6 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
 %
 \isadelimproof
 %
@@ -178,7 +176,6 @@
 can be split as above. The same is true for paired set comprehension:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -206,7 +203,6 @@
 The same proof procedure works for%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -231,7 +227,6 @@
 may be present in the goal. Consider the following function:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -285,7 +280,6 @@
 with the rewrite rule \isa{split{\isacharunderscore}paired{\isacharunderscore}all}:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -335,7 +329,6 @@
 where two separate \isa{simp} applications succeed.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \isadelimproof
 %
@@ -343,8 +336,7 @@
 %
 \isatagproof
 \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
-%
+{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}%
 \endisatagproof
 {\isafoldproof}%
 %
@@ -395,7 +387,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%