--- a/ProgTutorial/Recipes/Introspection.thy	Tue May 14 16:59:53 2019 +0200
+++ b/ProgTutorial/Recipes/Introspection.thy	Tue May 14 17:10:47 2019 +0200
@@ -3,9 +3,9 @@
 imports "../Appendix"
 begin
 
-section {* Introspection of Theorems and Proofs \label{rec:introspection} *}
+section \<open>Introspection of Theorems and Proofs \label{rec:introspection}\<close>
 
-text{* 
+text\<open>
   {\bf Problem:} 
   How to obtain all theorems that are used in the proof of a theorem?\smallskip
 
@@ -14,15 +14,15 @@
   To introspect a theorem, let us define the following three functions that 
   analyse the @{ML_type_ind proof_body} data-structure from the structure 
   @{ML_struct Proofterm}.
-*}
+\<close>
 
-ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms 
+ML %grayML\<open>fun pthms_of (PBody {thms, ...}) = map #2 thms 
 val get_names = (map Proofterm.thm_node_name) o pthms_of 
-val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of *}
+val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of\<close>
 
-text {* 
+text \<open>
   To see what their purpose is, consider the following three short proofs.
-*}
+\<close>
 
 lemma my_conjIa:
 shows "A \<and> B \<Longrightarrow> A \<and> B"
@@ -43,10 +43,10 @@
 apply(auto)
 done
 
-text {*
+text \<open>
   While the information about which theorems are used is obvious in
   the first two proofs, it is not obvious in the third, because of the
-  @{text auto}-step.  Fortunately, ``behind'' every proved theorem is
+  \<open>auto\<close>-step.  Fortunately, ``behind'' every proved theorem is
   a proof-tree that records all theorems that are employed for
   establishing this theorem.  We can traverse this proof-tree
   extracting this information.  Let us first extract the name of the
@@ -57,9 +57,9 @@
   |> Thm.proof_body_of
   |> get_names"
   "[\"Introspection.my_conjIa\"]"}
-*}
-text {*
-  whereby @{text "Introspection"} refers to the theory name in which
+\<close>
+text \<open>
+  whereby \<open>Introspection\<close> refers to the theory name in which
   we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind
   proof_body_of in Thm} returns a part of the data that is stored in a
   theorem.  Notice that the first proof above references
@@ -75,11 +75,11 @@
   |> List.concat"
   "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", 
   \"Pure.protectI\"]"}
-*}
-text {*
+\<close>
+text \<open>
   The theorems @{thm [source] protectD} and @{thm [source]
   protectI} that are internal theorems are always part of a
-  proof in Isabelle. Note also that applications of @{text assumption} do not
+  proof in Isabelle. Note also that applications of \<open>assumption\<close> do not
   count as a separate theorem, as you can see in the following code.
 
   @{ML_response_fake [display,gray]
@@ -89,8 +89,8 @@
   |> map get_names
   |> List.concat"
   "[\"Pure.protectD\", \"Pure.protectI\"]"}
-*}
-text {*
+\<close>
+text \<open>
   Interestingly, but not surprisingly, the proof of @{thm [source]
   my_conjIc} procceeds quite differently from @{thm [source] my_conjIa}
   and @{thm [source] my_conjIb}, as can be seen by the theorems that
@@ -105,8 +105,8 @@
   "[\"HOL.implies_True_equals\", \"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\", 
     \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\",
     \"Pure.protectI\"]"}
-*}
-text {*
+\<close>
+text \<open>
   Of course we can also descend into the second level of the tree 
   ``behind'' @{thm [source] my_conjIa} say, which
   means we obtain the theorems that are used in order to prove
@@ -123,14 +123,14 @@
   |> duplicates (op =)"
   "[\"\", \"Pure.protectD\",
  \"Pure.protectI\"]"}
-*}
-text {*
+\<close>
+text \<open>
   \begin{readmore} 
   The data-structure @{ML_type proof_body} is implemented
   in the file @{ML_file "Pure/proofterm.ML"}. The implementation 
   of theorems and related functions are in @{ML_file "Pure/thm.ML"}.  
   \end{readmore}
-*}
+\<close>