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