--- a/doc-src/TutorialI/CodeGen/CodeGen.thy Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy Tue Jul 17 13:46:21 2001 +0200
@@ -110,8 +110,8 @@
apply(induct_tac xs, simp, simp split: instr.split);
(*<*)done(*>*)
text{*\noindent
-Note that because both \isaindex{simp_all} and \isaindex{auto} perform simplification, they can
-be modified in the same way @{text 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 @{text simp}. Thus the proof can be
rewritten as
*}
(*<*)