--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Mon Oct 09 10:18:21 2000 +0200
@@ -98,14 +98,14 @@
that contains two \isa{case}-expressions over instructions. Thus we add
automatic case splitting as well, which finishes the proof:%
\end{isamarkuptxt}%
-\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
Note that because \isaindex{auto} performs simplification, it can
also be modified in the same way \isa{simp} can. Thus the proof can be
rewritten as%
\end{isamarkuptext}%
-\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
Although this is more compact, it is less clear for the reader of the proof.