diff -r 11aa41ed306d -r 1eced27ee0e1 doc-src/TutorialI/CTL/document/Base.tex
--- a/doc-src/TutorialI/CTL/document/Base.tex	Sun Aug 28 19:42:10 2005 +0200
+++ b/doc-src/TutorialI/CTL/document/Base.tex	Sun Aug 28 19:42:19 2005 +0200
@@ -7,6 +7,7 @@
 \endisadelimtheory
 %
 \isatagtheory
+\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -14,7 +15,6 @@
 \isadelimtheory
 %
 \endisadelimtheory
-\isamarkuptrue%
 %
 \isamarkupsection{Case Study: Verified Model Checking%
 }
@@ -74,9 +74,9 @@
 Abstracting from this concrete example, we assume there is a type of
 states:%
 \end{isamarkuptext}%
-\isamarkupfalse%
-\isacommand{typedecl}\ state\isamarkuptrue%
-%
+\isamarkuptrue%
+\isacommand{typedecl}\isamarkupfalse%
+\ state%
 \begin{isamarkuptext}%
 \noindent
 Command \commdx{typedecl} merely declares a new type but without
@@ -88,34 +88,36 @@
 reduces clutter.  Similarly we declare an arbitrary but fixed
 transition system, i.e.\ a relation between states:%
 \end{isamarkuptext}%
-\isamarkupfalse%
-\isacommand{consts}\ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequote}\isamarkuptrue%
-%
+\isamarkuptrue%
+\isacommand{consts}\isamarkupfalse%
+\ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent
 Again, we could have made \isa{M} a parameter of everything.
 Finally we introduce a type of atomic propositions%
 \end{isamarkuptext}%
-\isamarkupfalse%
-\isacommand{typedecl}\ atom\isamarkuptrue%
-%
+\isamarkuptrue%
+\isacommand{typedecl}\isamarkupfalse%
+\ atom%
 \begin{isamarkuptext}%
 \noindent
 and a \emph{labelling function}%
 \end{isamarkuptext}%
-\isamarkupfalse%
-\isacommand{consts}\ L\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ atom\ set{\isachardoublequote}\isamarkuptrue%
-%
+\isamarkuptrue%
+\isacommand{consts}\isamarkupfalse%
+\ L\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ {\isasymRightarrow}\ atom\ set{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent
 telling us which atomic propositions are true in each state.%
 \end{isamarkuptext}%
+\isamarkuptrue%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
+\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%