diff -r eacce1cd716a -r 05fc32a23b8b doc-src/TutorialI/CTL/document/Base.tex
--- a/doc-src/TutorialI/CTL/document/Base.tex	Tue Aug 16 13:42:21 2005 +0200
+++ b/doc-src/TutorialI/CTL/document/Base.tex	Tue Aug 16 13:42:23 2005 +0200
@@ -1,7 +1,20 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Base}%
-\isamarkupfalse%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isamarkuptrue%
 %
 \isamarkupsection{Case Study: Verified Model Checking%
 }
@@ -61,8 +74,8 @@
 Abstracting from this concrete example, we assume there is a type of
 states:%
 \end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{typedecl}\ state\isamarkupfalse%
+\isamarkupfalse%
+\isacommand{typedecl}\ state\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -75,30 +88,41 @@
 reduces clutter.  Similarly we declare an arbitrary but fixed
 transition system, i.e.\ a relation between states:%
 \end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+\isacommand{consts}\ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequote}\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \noindent
 Again, we could have made \isa{M} a parameter of everything.
 Finally we introduce a type of atomic propositions%
 \end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{typedecl}\ atom\isamarkupfalse%
+\isamarkupfalse%
+\isacommand{typedecl}\ atom\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \noindent
 and a \emph{labelling function}%
 \end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\ L\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ atom\ set{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+\isacommand{consts}\ L\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ atom\ set{\isachardoublequote}\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \noindent
 telling us which atomic propositions are true in each state.%
 \end{isamarkuptext}%
-\isamarkuptrue%
-\isamarkupfalse%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex