diff -r be23597e81db -r f875a25aa72d ProgTutorial/Solutions.thy
--- a/ProgTutorial/Solutions.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Solutions.thy	Fri May 17 10:38:01 2019 +0200
@@ -56,11 +56,11 @@
   as follows:
 
   @{ML_matchresult_fake [display,gray]
-  "@{prop \"\<forall>x y z. P x = P z\"}
+  \<open>@{prop "\<forall>x y z. P x = P z"}
   |> kill_trivial_quantifiers
   |> pretty_term @{context} 
-  |> pwriteln"
-  "\<forall>x z. P x = P z"}
+  |> pwriteln\<close>
+  \<open>\<forall>x z. P x = P z\<close>}
 \<close>
 
 
@@ -111,13 +111,13 @@
   normally return. For example:
 
   @{ML_matchresult [display,gray]
-"let
-  val input1 = (Symbol.explode \"foo bar\")
-  val input2 = (Symbol.explode \"foo (*test*) bar (*test*)\")
+\<open>let
+  val input1 = (Symbol.explode "foo bar")
+  val input2 = (Symbol.explode "foo (*test*) bar (*test*)")
 in
   (scan_all input1, scan_all input2)
-end"
-"(\"foo bar\", \"foo (**test**) bar (**test**)\")"}
+end\<close>
+\<open>("foo bar", "foo (**test**) bar (**test**)")\<close>}
 \<close>
 
 text \<open>\solution{ex:contextfree}\<close>
@@ -331,8 +331,8 @@
   This function generates for example:
 
   @{ML_matchresult_fake [display,gray] 
-  "pwriteln (pretty_term @{context} (term_tree 2))" 
-  "(1 + 2) + (3 + 4)"} 
+  \<open>pwriteln (pretty_term @{context} (term_tree 2))\<close> 
+  \<open>(1 + 2) + (3 + 4)\<close>} 
 
   The next function constructs a goal of the form \<open>P \<dots>\<close> with a term 
   produced by @{ML term_tree} filled in.
@@ -344,7 +344,7 @@
   Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define
   two tactics, \<open>c_tac\<close> and \<open>s_tac\<close>, for the conversion and simproc,
   respectively. The idea is to first apply the conversion (respectively simproc) and 
-  then prove the remaining goal using @{ML "cheat_tac" in Skip_Proof}.
+  then prove the remaining goal using @{ML \<open>cheat_tac\<close> in Skip_Proof}.
 \<close>
 
 ML Skip_Proof.cheat_tac