--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Sun Jan 30 20:48:50 2005 +0100
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Tue Feb 01 18:01:57 2005 +0100
@@ -105,27 +105,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}value\ e\ s{\isacharparenright}\ {\isacharhash}\ vs{\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptxt}%
-\noindent
-It will be proved by induction on \isa{e} followed by simplification.
-First, we must prove a lemma about executing the concatenation of two
-instruction sequences:%
-\end{isamarkuptxt}%
\isamarkuptrue%
\isamarkupfalse%
\isacommand{lemma}\ exec{\isacharunderscore}app{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}xs{\isacharat}ys{\isacharparenright}\ s\ vs\ {\isacharequal}\ exec\ ys\ s\ {\isacharparenleft}exec\ xs\ s\ vs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptxt}%
-\noindent
-This requires induction on \isa{xs} and ordinary simplification for the
-base cases. In the induction step, simplification leaves us with a formula
-that contains two \isa{case}-expressions over instructions. Thus we add
-automatic case splitting, which finishes the proof:%
-\end{isamarkuptxt}%
\isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -137,7 +122,7 @@
\isamarkuptrue%
\isamarkupfalse%
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%