diff -r bda7527ccf05 -r cc2d676d5395 src/Doc/Tutorial/CodeGen/CodeGen.thy
--- a/src/Doc/Tutorial/CodeGen/CodeGen.thy	Wed Dec 26 16:07:28 2018 +0100
+++ b/src/Doc/Tutorial/CodeGen/CodeGen.thy	Wed Dec 26 16:25:20 2018 +0100
@@ -37,7 +37,7 @@
 The stack machine has three instructions: load a constant value onto the
 stack, load the contents of an address onto the stack, and apply a
 binary operation to the two topmost elements of the stack, replacing them by
-the result. As for @{text"expr"}, addresses and values are type parameters:
+the result. As for \<open>expr\<close>, addresses and values are type parameters:
 \<close>
 
 datatype (dead 'a, 'v) instr = Const 'v
@@ -46,7 +46,7 @@
 
 text\<open>
 The execution of the stack machine is modelled by a function
-@{text"exec"} that takes a list of instructions, a store (modelled as a
+\<open>exec\<close> that takes a list of instructions, a store (modelled as a
 function from addresses to values, just like the environment for
 evaluating expressions), and a stack (modelled as a list) of values,
 and returns the stack at the end of the execution --- the store remains
@@ -103,14 +103,14 @@
 txt\<open>\noindent
 This requires induction on @{term"xs"} and ordinary simplification for the
 base cases. In the induction step, simplification leaves us with a formula
-that contains two @{text"case"}-expressions over instructions. Thus we add
+that contains two \<open>case\<close>-expressions over instructions. Thus we add
 automatic case splitting, which finishes the proof:
 \<close>
 apply(induct_tac xs, simp, simp split: instr.split)
 (*<*)done(*>*)
 text\<open>\noindent
 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
+be modified in the same way as \<open>simp\<close>.  Thus the proof can be
 rewritten as
 \<close>
 (*<*)