diff -r be23597e81db -r f875a25aa72d ProgTutorial/Package/Ind_Code.thy
--- a/ProgTutorial/Package/Ind_Code.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Fri May 17 10:38:01 2019 +0200
@@ -494,13 +494,13 @@
   the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows:
 
   @{ML_matchresult_fake [display, gray]
-"let
-  val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]
+\<open>let
+  val ctrms = [@{cterm "a::nat"}, @{cterm "b::nat"}, @{cterm "c::nat"}]
   val new_thm = all_elims ctrms @{thm all_elims_test}
 in
   pwriteln (pretty_thm_no_vars @{context} new_thm)
-end"
-  "P a b c"}
+end\<close>
+  \<open>P a b c\<close>}
 
   Note the difference with @{ML inst_spec_tac} from Page~\pageref{fun:instspectac}:
   @{ML inst_spec_tac} is a tactic which operates on a goal state; in contrast
@@ -511,12 +511,12 @@
   @{thm [source] imp_elims_test}:
 
   @{ML_matchresult_fake [display, gray]
-"let
+\<open>let
   val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}
 in
   pwriteln (pretty_thm_no_vars @{context} res)
-end"
-  "C"}
+end\<close>
+  \<open>C\<close>}
 
   Now we set up the proof for the introduction rule as follows:
 \<close>
@@ -728,7 +728,7 @@
   whether we are in the simple or complicated case by checking whether
   the topmost connective is an \<open>\<forall>\<close>. The premises in the simple
   case cannot have such a quantification, since the first step 
-  of @{ML "expand_tac"} was to ``rulify'' the lemma. 
+  of @{ML \<open>expand_tac\<close>} was to ``rulify'' the lemma. 
   The premise of the complicated case must have at least one  \<open>\<forall>\<close>
   coming from the quantification over the \<open>preds\<close>. So 
   we can implement the following function
@@ -1011,7 +1011,7 @@
   any name.} Line 21 registers the induction principles. For this we have
   to use some specific attributes. The first @{ML_ind  case_names in Rule_Cases} 
   corresponds to the case names that are used by Isar to reference the proof
-  obligations in the induction. The second @{ML "consumes 1" in Rule_Cases}
+  obligations in the induction. The second @{ML \<open>consumes 1\<close> in Rule_Cases}
   indicates that the first premise of the induction principle (namely
   the predicate over which the induction proceeds) is eliminated.