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