--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Tue Jul 17 13:46:21 2001 +0200
@@ -102,8 +102,8 @@
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
-Note that because both \isaindex{simp_all} and \isaindex{auto} perform simplification, they can
-be modified in the same way \isa{simp} can. Thus the proof can be
+Note that because both \methdx{simp_all} and \methdx{auto} perform simplification, they can
+be modified in the same way as \isa{simp}. Thus the proof can be
rewritten as%
\end{isamarkuptext}%
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%