updated;

--- a/doc-src/AxClass/Group/document/Group.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/AxClass/Group/document/Group.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,6 +1,7 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Group}%
+\isamarkupfalse%
 %
 \isamarkupheader{Basic group theory%
 }

--- a/doc-src/AxClass/Group/document/Product.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/AxClass/Group/document/Product.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,6 +1,7 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Product}%
+\isamarkupfalse%
 %
 \isamarkupheader{Syntactic classes%
 }

--- a/doc-src/AxClass/Group/document/Semigroups.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/AxClass/Group/document/Semigroups.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,6 +1,7 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Semigroups}%
+\isamarkupfalse%
 %
 \isamarkupheader{Semigroups%
 }

--- a/doc-src/AxClass/Group/document/isabelle.sty	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/AxClass/Group/document/isabelle.sty	Mon Aug 29 11:44:23 2005 +0200
@@ -22,10 +22,10 @@
 \newcommand{\isamath}[1]{\emph{$#1$}}
 \newcommand{\isatext}[1]{\emph{#1}}
 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
-\newcommand{\isactrlsub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlsup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlisub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlisup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
+\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
 \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
 \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
@@ -89,6 +89,8 @@
 \chardef\isacharbar=`\|
 \chardef\isacharbraceright=`\}
 \chardef\isachartilde=`\~
+\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}
+\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}
 
 
 % keyword and section markup
@@ -165,6 +167,8 @@
 \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
 \renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
 \renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
+\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
+\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
 }
 
 \newcommand{\isabellestylesl}{%

--- a/doc-src/AxClass/Nat/document/NatClass.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/AxClass/Nat/document/NatClass.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,6 +1,7 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{NatClass}%
+\isamarkupfalse%
 %
 \isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}%
 }

--- a/doc-src/IsarOverview/Isar/document/Induction.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/IsarOverview/Isar/document/Induction.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Induction}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -120,7 +120,6 @@
 natural number (remember: $0-1=0$):%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
 \isacommand{lemma}\isamarkupfalse%
 \ {\isachardoublequoteopen}length{\isacharparenleft}tl\ xs{\isacharparenright}\ {\isacharequal}\ length\ xs\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
 %
@@ -653,7 +652,6 @@
 The proof is so simple that it can be condensed to%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \isadelimproof
 %
@@ -675,7 +673,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/IsarOverview/Isar/document/Logic.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/IsarOverview/Isar/document/Logic.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Logic}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -1151,7 +1151,6 @@
 \endisadelimML
 %
 \isatagML
-\isamarkupfalse%
 %
 \endisatagML
 {\isafoldML}%
@@ -1310,7 +1309,6 @@
 \isamarkuptrue%
 %
 \renewcommand{\isamarkupcmt}[1]{#1}
-\isamarkupfalse%
 %
 \isadelimproof
 %
@@ -1320,8 +1318,7 @@
 \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}\isanewline
 \ \ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}P\isactrlisub {\isadigit{1}}\ {\isasymor}\ P\isactrlisub {\isadigit{2}}\ {\isasymor}\ P\isactrlisub {\isadigit{3}}{\isachardoublequoteclose}\ \isamarkupfalse%
-\ %
+\ {\isachardoublequoteopen}P\isactrlisub {\isadigit{1}}\ {\isasymor}\ P\isactrlisub {\isadigit{2}}\ {\isasymor}\ P\isactrlisub {\isadigit{3}}{\isachardoublequoteclose}\ \ %
 \isamarkupcmt{\dots%
 }
 \isanewline
@@ -1335,8 +1332,7 @@
 }
 \isanewline
 \ \ \ \ \isacommand{have}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isamarkupfalse%
-\ %
+\ {\isacharquery}thesis\ \ %
 \isamarkupcmt{\dots%
 }
 \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
@@ -1351,8 +1347,7 @@
 }
 \isanewline
 \ \ \ \ \isacommand{have}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isamarkupfalse%
-\ %
+\ {\isacharquery}thesis\ \ %
 \isamarkupcmt{\dots%
 }
 \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
@@ -1367,8 +1362,7 @@
 }
 \isanewline
 \ \ \ \ \isacommand{have}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isamarkupfalse%
-\ %
+\ {\isacharquery}thesis\ \ %
 \isamarkupcmt{\dots%
 }
 \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
@@ -1450,7 +1444,6 @@
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -1472,7 +1465,6 @@
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -1541,8 +1533,7 @@
 \ \ \isacommand{from}\isamarkupfalse%
 \ A\ \isacommand{obtain}\isamarkupfalse%
 \ x\ y\ \isakeyword{where}\ P{\isacharcolon}\ {\isachardoublequoteopen}P\ x\ y{\isachardoublequoteclose}\ \isakeyword{and}\ Q{\isacharcolon}\ {\isachardoublequoteopen}Q\ x\ y{\isachardoublequoteclose}\ \ \isacommand{by}\isamarkupfalse%
-\ blast\isamarkupfalse%
-%
+\ blast%
 \endisatagproof
 {\isafoldproof}%
 %
@@ -1614,7 +1605,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/IsarOverview/Isar/document/isabelle.sty	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/IsarOverview/Isar/document/isabelle.sty	Mon Aug 29 11:44:23 2005 +0200
@@ -22,10 +22,10 @@
 \newcommand{\isamath}[1]{\emph{$#1$}}
 \newcommand{\isatext}[1]{\emph{#1}}
 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
-\newcommand{\isactrlsub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlsup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlisub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlisup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
+\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
 \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
 \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
@@ -89,6 +89,8 @@
 \chardef\isacharbar=`\|
 \chardef\isacharbraceright=`\}
 \chardef\isachartilde=`\~
+\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}
+\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}
 
 
 % keyword and section markup
@@ -165,6 +167,8 @@
 \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
 \renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
 \renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
+\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
+\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
 }
 
 \newcommand{\isabellestylesl}{%

--- a/doc-src/Locales/Locales/document/Locales.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/Locales/Locales/document/Locales.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,6 +1,7 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Locales}%
+\isamarkupfalse%
 %
 \isadelimtheory
 \isanewline
@@ -8,7 +9,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -22,7 +22,6 @@
 \endisadelimML
 %
 \isatagML
-\isamarkupfalse%
 %
 \endisatagML
 {\isafoldML}%
@@ -460,7 +459,6 @@
 \endisadelimML
 %
 \isatagML
-\isamarkupfalse%
 %
 \endisatagML
 {\isafoldML}%
@@ -1309,7 +1307,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/Locales/Locales/document/isabelle.sty	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/Locales/Locales/document/isabelle.sty	Mon Aug 29 11:44:23 2005 +0200
@@ -22,10 +22,10 @@
 \newcommand{\isamath}[1]{\emph{$#1$}}
 \newcommand{\isatext}[1]{\emph{#1}}
 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
-\newcommand{\isactrlsub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlsup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlisub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlisup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
+\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
 \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
 \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
@@ -89,6 +89,8 @@
 \chardef\isacharbar=`\|
 \chardef\isacharbraceright=`\}
 \chardef\isachartilde=`\~
+\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}
+\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}
 
 
 % keyword and section markup
@@ -165,6 +167,8 @@
 \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
 \renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
 \renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
+\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
+\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
 }
 
 \newcommand{\isabellestylesl}{%

--- a/doc-src/TutorialI/Advanced/document/Partial.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Partial}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -339,7 +339,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{WFrec}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -150,8 +150,6 @@
 crucial hint\cmmdx{hints} to our definition:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
-\isamarkupfalse%
 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
@@ -169,7 +167,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Advanced/document/simp.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Advanced/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}%
@@ -236,7 +236,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/CTL/document/Base.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/CTL/document/Base.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Base}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -117,7 +117,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/CTL/document/CTL.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{CTL}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -29,7 +29,6 @@
 \isa{formula} by a new constructor%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula%
 \begin{isamarkuptext}%
 \noindent
@@ -51,8 +50,6 @@
 a new datatype and a new function.}%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
-\isamarkupfalse%
 {\isachardoublequoteopen}s\ {\isasymTurnstile}\ AF\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent
@@ -69,8 +66,6 @@
 \isa{mc\ f} and all states all of whose direct successors are in \isa{T}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
-\isamarkupfalse%
 {\isachardoublequoteopen}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent
@@ -98,15 +93,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -114,27 +106,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -392,28 +369,12 @@
 where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -518,8 +479,7 @@
 \isacommand{primrec}\isamarkupfalse%
 \isanewline
 {\isachardoublequoteopen}until\ A\ B\ s\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}until\ A\ B\ s\ {\isacharparenleft}t{\isacharhash}p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ A\ {\isasymand}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ until\ A\ B\ t\ p{\isacharparenright}{\isachardoublequoteclose}\isamarkupfalse%
-%
+{\isachardoublequoteopen}until\ A\ B\ s\ {\isacharparenleft}t{\isacharhash}p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ A\ {\isasymand}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ until\ A\ B\ t\ p{\isacharparenright}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent
 Expressing the semantics of \isa{EU} is now straightforward:
@@ -546,21 +506,12 @@
 For more CTL exercises see, for example, Huth and Ryan \cite{Huth-Ryan-book}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -568,16 +519,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -585,24 +532,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -631,7 +566,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/CTL/document/CTLind.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{CTLind}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -137,8 +137,7 @@
 \ \isacommand{apply}\isamarkupfalse%
 {\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline
 \ \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}clarsimp{\isacharparenright}\isamarkupfalse%
-%
+{\isacharparenleft}clarsimp{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
 \begin{isabelle}%
@@ -239,7 +238,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/CTL/document/PDL.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/CTL/document/PDL.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{PDL}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -145,8 +145,7 @@
 \ \isacommand{apply}\isamarkupfalse%
 {\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
 \ \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse%
-%
+{\isacharparenleft}simp{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
 Simplification leaves us with the following first subgoal
@@ -293,16 +292,12 @@
 \index{PDL|)}%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -310,15 +305,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -326,17 +318,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -350,7 +337,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{CodeGen}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -116,7 +116,6 @@
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -145,7 +144,6 @@
 instruction sequences:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -171,8 +169,7 @@
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse%
-%
+{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
 \endisatagproof
 {\isafoldproof}%
 %
@@ -187,8 +184,6 @@
 rewritten as%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \isadelimproof
 %
@@ -196,8 +191,7 @@
 %
 \isatagproof
 \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse%
-%
+{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
 \endisatagproof
 {\isafoldproof}%
 %
@@ -216,14 +210,12 @@
 \index{compiling expressions example|)}%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -237,7 +229,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{ABexpr}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -130,8 +130,7 @@
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \isacommand{apply}\isamarkupfalse%
-\ simp{\isacharunderscore}all\isamarkupfalse%
-%
+\ simp{\isacharunderscore}all%
 \endisatagproof
 {\isafoldproof}%
 %
@@ -161,18 +160,12 @@
 \end{exercise}%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -180,18 +173,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -205,7 +192,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Fundata}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -72,14 +72,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 \noindent
@@ -92,7 +90,6 @@
 \end{isabelle}%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -106,7 +103,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Nested}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -26,7 +26,6 @@
 where function symbols can be applied to a list of arguments:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
 \isacommand{datatype}\isamarkupfalse%
 \ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}{\isachardoublequoteopen}term{\isachardoublequoteclose}\ {\isacharequal}\ Var\ {\isacharprime}v\ {\isacharbar}\ App\ {\isacharprime}f\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
@@ -140,16 +139,12 @@
 that the suggested equation holds:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -157,17 +152,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -175,15 +165,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -243,7 +230,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{unfoldnested}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -23,7 +23,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Documents/document/Documents.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Documents}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -156,14 +156,12 @@
   specifies an Isabelle symbol for the new operator:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \isadelimML
 %
 \endisadelimML
 %
 \isatagML
-\isamarkupfalse%
 %
 \endisatagML
 {\isafoldML}%
@@ -174,8 +172,7 @@
 \isacommand{constdefs}\isamarkupfalse%
 \isanewline
 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ {\isachardoublequoteopen}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}\isamarkupfalse%
-%
+\ \ {\isachardoublequoteopen}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent The X-Symbol package within Proof~General provides several
   input methods to enter \isa{{\isasymoplus}} in the text.  If all fails one may
@@ -189,14 +186,12 @@
   consider the following hybrid declaration of \isa{xor}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \isadelimML
 %
 \endisadelimML
 %
 \isatagML
-\isamarkupfalse%
 %
 \endisatagML
 {\isafoldML}%
@@ -211,8 +206,7 @@
 \isanewline
 \isacommand{syntax}\isamarkupfalse%
 \ {\isacharparenleft}xsymbols{\isacharparenright}\isanewline
-\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
-%
+\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}%
 \begin{isamarkuptext}%
 The \commdx{syntax} command introduced here acts like
   \isakeyword{consts}, but without declaring a logical constant.  The
@@ -918,7 +912,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Ifexpr}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -180,7 +180,6 @@
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -203,8 +202,6 @@
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -212,15 +209,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -259,8 +253,6 @@
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -268,15 +260,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -303,21 +292,12 @@
 \index{boolean expressions example|)}%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -325,15 +305,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -341,15 +318,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -357,15 +331,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -379,7 +350,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Inductive/document/AB.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Inductive/document/AB.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{AB}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -309,8 +309,7 @@
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse%
-%
+{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
 The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction
@@ -325,8 +324,7 @@
 \isacommand{apply}\isamarkupfalse%
 {\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
 \ \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
-%
+{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
 Simplification disposes of the base case and leaves only a conjunction
@@ -452,7 +450,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Inductive/document/Advanced.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Inductive/document/Advanced.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,6 +1,7 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Advanced}%
+\isamarkupfalse%
 %
 \isadelimtheory
 \isanewline

--- a/doc-src/TutorialI/Inductive/document/Even.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Inductive/document/Even.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,6 +1,7 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Even}%
+\isamarkupfalse%
 %
 \isadelimtheory
 \isanewline

--- a/doc-src/TutorialI/Inductive/document/Mutual.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Inductive/document/Mutual.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Mutual}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -80,13 +80,6 @@
 We do not show the proof script.%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -100,7 +93,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Inductive/document/Star.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Inductive/document/Star.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Star}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -135,7 +135,6 @@
 transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -283,17 +282,12 @@
 \end{exercise}%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -307,7 +301,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{AdvancedInd}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -82,7 +82,6 @@
 result to the usual \isa{{\isasymLongrightarrow}} form:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -97,7 +96,6 @@
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 \noindent
@@ -155,7 +153,6 @@
 the notation $\overline{y}$ is merely an informal device.%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -303,7 +300,6 @@
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -432,7 +428,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Misc/document/Itrev.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Itrev}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -111,7 +111,6 @@
 just not true.  The correct generalization is%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -126,7 +125,6 @@
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 \noindent
@@ -151,7 +149,6 @@
 for all \isa{ys} instead of a fixed one:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -166,7 +163,6 @@
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -216,7 +212,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Misc/document/Option2.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/Option2.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Option{\isadigit{2}}}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -15,8 +15,6 @@
 \isadelimtheory
 %
 \endisadelimtheory
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \indexbold{*option (type)}\indexbold{*None (constant)}%
@@ -45,7 +43,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Misc/document/Plus.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/Plus.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Plus}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -30,15 +30,12 @@
 \noindent and prove%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -53,7 +50,6 @@
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -67,7 +63,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Misc/document/Tree.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Tree}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -22,9 +22,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{datatype}\isamarkupfalse%
-\ {\isacharprime}a\ tree\ {\isacharequal}\ Tip\ {\isacharbar}\ Node\ {\isachardoublequoteopen}{\isacharprime}a\ tree{\isachardoublequoteclose}\ {\isacharprime}a\ {\isachardoublequoteopen}{\isacharprime}a\ tree{\isachardoublequoteclose}\isamarkupfalse%
-\isamarkupfalse%
-%
+\ {\isacharprime}a\ tree\ {\isacharequal}\ Tip\ {\isacharbar}\ Node\ {\isachardoublequoteopen}{\isacharprime}a\ tree{\isachardoublequoteclose}\ {\isacharprime}a\ {\isachardoublequoteopen}{\isacharprime}a\ tree{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent
 Define a function \isa{mirror} that mirrors a binary tree
@@ -38,8 +36,6 @@
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -47,8 +43,6 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -63,8 +57,6 @@
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -78,7 +70,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Misc/document/Tree2.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree2.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Tree{\isadigit{2}}}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -25,21 +25,17 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{consts}\isamarkupfalse%
-\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\isamarkupfalse%
-%
+\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent Define \isa{flatten{\isadigit{2}}} and prove%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -54,7 +50,6 @@
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -68,7 +63,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Misc/document/appendix.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/appendix.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{appendix}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -53,7 +53,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{case{\isacharunderscore}exprs}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -100,8 +100,7 @@
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
-%
+{\isacharparenleft}auto{\isacharparenright}%
 \endisatagproof
 {\isafoldproof}%
 %
@@ -135,7 +134,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Misc/document/fakenat.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/fakenat.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{fakenat}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -29,7 +29,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Misc/document/natsum.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{natsum}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -118,7 +118,6 @@
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -141,7 +140,6 @@
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -169,8 +167,7 @@
 %
 \isatagproof
 \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}arith{\isacharparenright}\isamarkupfalse%
-%
+{\isacharparenleft}arith{\isacharparenright}%
 \endisatagproof
 {\isafoldproof}%
 %
@@ -190,7 +187,6 @@
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -224,7 +220,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Misc/document/pairs.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Misc/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}%
@@ -52,7 +52,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Misc/document/prime_def.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/prime_def.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{prime{\isacharunderscore}def}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -15,7 +15,6 @@
 \isadelimtheory
 %
 \endisadelimtheory
-\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \begin{warn}
@@ -41,7 +40,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- 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}%

--- a/doc-src/TutorialI/Misc/document/types.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/types.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{types}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -76,7 +76,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Induction}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -108,7 +108,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Recdef/document/Nested0.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Nested{\isadigit{0}}}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -42,7 +42,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Recdef/document/Nested1.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Nested{\isadigit{1}}}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -62,7 +62,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Nested{\isadigit{2}}}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -32,7 +32,6 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -116,8 +115,6 @@
 the recursion equations:\cmmdx{hints}%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
-\isamarkupfalse%
 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
@@ -142,7 +139,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Recdef/document/examples.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/examples.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{examples}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -120,7 +120,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{simplification}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -158,7 +158,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Recdef/document/termination.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{termination}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -60,14 +60,11 @@
 simplification rule.\cmmdx{hints}%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
-\isamarkupfalse%
 \isacommand{recdef}\isamarkupfalse%
 \ qs\ {\isachardoublequoteopen}measure\ length{\isachardoublequoteclose}\isanewline
 \ {\isachardoublequoteopen}qs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
 \ {\isachardoublequoteopen}qs{\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ y{\isasymle}x{\isacharparenright}\ xs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharat}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ x{\isacharless}y{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
-{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le{\isacharparenright}\isamarkupfalse%
-%
+{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 This time everything works fine. Now \isa{qs{\isachardot}simps} contains precisely
@@ -111,7 +108,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Rules/document/find2.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Rules/document/find2.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{find{\isadigit{2}}}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -15,7 +15,6 @@
 \isadelimtheory
 %
 \endisadelimtheory
-\isamarkupfalse%
 %
 \isadelimproof
 %
@@ -42,7 +41,6 @@
 database.  Given the goal%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -50,7 +48,6 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
 %
 \isadelimproof
 %
@@ -78,7 +75,6 @@
 into account, too.%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -92,7 +88,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,6 +1,7 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{ToyList}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
@@ -248,7 +249,6 @@
 In order to simplify this subgoal further, a lemma suggests itself.%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -304,7 +304,6 @@
 embarking on the proof of a lemma usually remains implicit.%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -398,7 +397,6 @@
 and the missing lemma is associativity of \isa{{\isacharat}}.%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%

--- a/doc-src/TutorialI/Trie/document/Trie.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Trie}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -218,18 +218,12 @@
 \end{exercise}%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -237,18 +231,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -256,18 +244,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -275,22 +257,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -298,18 +270,12 @@
 \isadelimproof
 %
 \endisadelimproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
@@ -323,7 +289,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Types/document/Axioms.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Axioms.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Axioms}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -374,7 +374,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Types/document/Numbers.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,6 +1,7 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Numbers}%
+\isamarkupfalse%
 %
 \isadelimtheory
 \isanewline
@@ -560,7 +561,7 @@
 %
 \isatagML
 \isacommand{ML}\isamarkupfalse%
-{\isacharbraceleft}{\isacharasterisk}set\ show{\isacharunderscore}sorts{\isacharasterisk}{\isacharbraceright}%
+{\isacharverbatimopen}set\ show{\isacharunderscore}sorts{\isacharverbatimclose}%
 \endisatagML
 {\isafoldML}%
 %
@@ -585,7 +586,7 @@
 %
 \isatagML
 \isacommand{ML}\isamarkupfalse%
-{\isacharbraceleft}{\isacharasterisk}reset\ show{\isacharunderscore}sorts{\isacharasterisk}{\isacharbraceright}%
+{\isacharverbatimopen}reset\ show{\isacharunderscore}sorts{\isacharverbatimclose}%
 \endisatagML
 {\isafoldML}%
 %

--- a/doc-src/TutorialI/Types/document/Overloading.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Overloading}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -53,7 +53,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Types/document/Overloading0.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading0.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Overloading{\isadigit{0}}}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -68,7 +68,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Types/document/Overloading1.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading1.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Overloading{\isadigit{1}}}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -126,7 +126,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Types/document/Overloading2.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Overloading{\isadigit{2}}}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -83,7 +83,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- 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}%

--- a/doc-src/TutorialI/Types/document/Records.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Records.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,6 +1,7 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Records}%
+\isamarkupfalse%
 %
 \isamarkupheader{Records \label{sec:records}%
 }
@@ -11,7 +12,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -653,7 +653,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/Types/document/Typedefs.tex	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Typedefs.tex	Mon Aug 29 11:44:23 2005 +0200
@@ -1,13 +1,13 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Typedefs}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -329,7 +329,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/TutorialI/isabelle.sty	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/TutorialI/isabelle.sty	Mon Aug 29 11:44:23 2005 +0200
@@ -22,10 +22,10 @@
 \newcommand{\isamath}[1]{\emph{$#1$}}
 \newcommand{\isatext}[1]{\emph{#1}}
 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
-\newcommand{\isactrlsub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlsup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlisub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlisup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
+\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
 \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
 \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
@@ -89,6 +89,8 @@
 \chardef\isacharbar=`\|
 \chardef\isacharbraceright=`\}
 \chardef\isachartilde=`\~
+\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}
+\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}
 
 
 % keyword and section markup
@@ -165,6 +167,8 @@
 \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
 \renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
 \renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
+\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
+\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
 }
 
 \newcommand{\isabellestylesl}{%

--- a/doc-src/ZF/isabelle.sty	Mon Aug 29 10:28:17 2005 +0200
+++ b/doc-src/ZF/isabelle.sty	Mon Aug 29 11:44:23 2005 +0200
@@ -22,10 +22,10 @@
 \newcommand{\isamath}[1]{\emph{$#1$}}
 \newcommand{\isatext}[1]{\emph{#1}}
 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
-\newcommand{\isactrlsub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlsup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlisub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlisup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
+\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
 \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
 \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
@@ -89,6 +89,8 @@
 \chardef\isacharbar=`\|
 \chardef\isacharbraceright=`\}
 \chardef\isachartilde=`\~
+\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}
+\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}
 
 
 % keyword and section markup
@@ -165,6 +167,8 @@
 \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
 \renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
 \renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
+\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
+\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
 }
 
 \newcommand{\isabellestylesl}{%