diff -r 5b6305cab436 -r 9feb1e0c4cb3 doc-src/TutorialI/CodeGen/CodeGen.thy
--- a/doc-src/TutorialI/CodeGen/CodeGen.thy	Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy	Tue Sep 12 15:43:15 2000 +0200
@@ -111,11 +111,11 @@
 
 text{*\noindent
 Note that because \isaindex{auto} performs simplification, it can
-also be modified in the same way @{text"simp"} can. Thus the proof can be
+also be modified in the same way @{text simp} can. Thus the proof can be
 rewritten as
 *}
 (*<*)
-lemmas [simp del] = exec_app;
+declare exec_app[simp del];
 lemma [simp]: "\\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
 (*>*)
 by(induct_tac xs, auto split: instr.split);