--- a/ProgTutorial/Recipes/Introspection.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/Introspection.thy	Fri May 17 10:38:01 2019 +0200
@@ -53,10 +53,10 @@
   established theorem. This can be done with
 
   @{ML_matchresult [display,gray]
-  "@{thm my_conjIa}
+  \<open>@{thm my_conjIa}
   |> Thm.proof_body_of
-  |> get_names"
-  "[\"Introspection.my_conjIa\"]"}
+  |> get_names\<close>
+  \<open>["Introspection.my_conjIa"]\<close>}
 \<close>
 text \<open>
   whereby \<open>Introspection\<close> refers to the theory name in which
@@ -68,13 +68,13 @@
   first level of the proof-tree, as follows.
 
   @{ML_matchresult_fake [display,gray]
-  "@{thm my_conjIa}
+  \<open>@{thm my_conjIa}
   |> Thm.proof_body_of
   |> get_pbodies
   |> map get_names
-  |> List.concat"
-  "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", 
-  \"Pure.protectI\"]"}
+  |> List.concat\<close>
+  \<open>["HOL.conjunct2", "HOL.conjunct1", "HOL.conjI", "Pure.protectD", 
+  "Pure.protectI"]\<close>}
 \<close>
 text \<open>
   The theorems @{thm [source] protectD} and @{thm [source]
@@ -83,12 +83,12 @@
   count as a separate theorem, as you can see in the following code.
 
   @{ML_matchresult_fake [display,gray]
-  "@{thm my_conjIb}
+  \<open>@{thm my_conjIb}
   |> Thm.proof_body_of
   |> get_pbodies
   |> map get_names
-  |> List.concat"
-  "[\"Pure.protectD\", \"Pure.protectI\"]"}
+  |> List.concat\<close>
+  \<open>["Pure.protectD", "Pure.protectI"]\<close>}
 \<close>
 text \<open>
   Interestingly, but not surprisingly, the proof of @{thm [source]
@@ -97,14 +97,14 @@
   are returned for @{thm [source] my_conjIc}.
 
   @{ML_matchresult_fake [display,gray]
-  "@{thm my_conjIc}
+  \<open>@{thm my_conjIc}
   |> Thm.proof_body_of
   |> get_pbodies
   |> map get_names
-  |> List.concat"
-  "[\"HOL.implies_True_equals\", \"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\", 
-    \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\",
-    \"Pure.protectI\"]"}
+  |> List.concat\<close>
+  \<open>["HOL.implies_True_equals", "HOL.Eq_TrueI", "HOL.simp_thms_25", "HOL.eq_reflection", 
+    "HOL.conjunct2", "HOL.conjunct1", "HOL.TrueI", "Pure.protectD",
+    "Pure.protectI"]\<close>}
 \<close>
 text \<open>
   Of course we can also descend into the second level of the tree 
@@ -113,16 +113,16 @@
   @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
 
   @{ML_matchresult_fake [display, gray]
-  "@{thm my_conjIa}
+  \<open>@{thm my_conjIa}
   |> Thm.proof_body_of
   |> get_pbodies
   |> map get_pbodies
   |> (map o map) get_names
   |> List.concat
   |> List.concat
-  |> duplicates (op =)"
-  "[\"\", \"Pure.protectD\",
- \"Pure.protectI\"]"}
+  |> duplicates (op =)\<close>
+  \<open>["", "Pure.protectD",
+ "Pure.protectI"]\<close>}
 \<close>