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