--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Sun Jan 30 20:48:50 2005 +0100
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Tue Feb 01 18:01:57 2005 +0100
@@ -103,14 +103,9 @@
\isacommand{lemma}\ {\isachardoublequote}evala\ {\isacharparenleft}substa\ s\ a{\isacharparenright}\ env\ {\isacharequal}\ evala\ a\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ evala\ {\isacharparenleft}s\ x{\isacharparenright}\ env{\isacharparenright}\ {\isasymand}\isanewline
\ \ \ \ \ \ \ \ evalb\ {\isacharparenleft}substb\ s\ b{\isacharparenright}\ env\ {\isacharequal}\ evalb\ b\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ evala\ {\isacharparenleft}s\ x{\isacharparenright}\ env{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ a\ \isakeyword{and}\ b{\isacharparenright}\isamarkupfalse%
-%
-\begin{isamarkuptxt}%
-\noindent
-The resulting 8 goals (one for each constructor) are proved in one fell swoop:%
-\end{isamarkuptxt}%
+\isamarkupfalse%
\isamarkuptrue%
-\isacommand{apply}\ simp{\isacharunderscore}all\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%