diff -r be23597e81db -r f875a25aa72d ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Tactical.thy	Fri May 17 10:38:01 2019 +0200
@@ -48,17 +48,17 @@
   This proof translates to the following ML-code.
   
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val ctxt = @{context}
-  val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
+  val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}
 in
-  Goal.prove ctxt [\"P\", \"Q\"] [] goal 
+  Goal.prove ctxt ["P", "Q"] [] goal 
    (fn _ =>  eresolve_tac @{context} [@{thm disjE}] 1
              THEN resolve_tac @{context} [@{thm disjI2}] 1
              THEN assume_tac @{context} 1
              THEN resolve_tac @{context} [@{thm disjI1}] 1
              THEN assume_tac @{context} 1)
-end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
+end\<close> \<open>?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P\<close>}
   
   To start the proof, the function @{ML_ind prove in Goal} sets up a goal
   state for proving the goal @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. We can give this
@@ -764,16 +764,16 @@
   The function @{ML_ind RS in Drule}, for example, does this.
   
   @{ML_matchresult_fake [display,gray]
-  "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
+  \<open>@{thm disjI1} RS @{thm conjI}\<close> \<open>\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q\<close>}
 
   In this example it instantiates the first premise of the \<open>conjI\<close>-theorem 
   with the theorem \<open>disjI1\<close>. If the instantiation is impossible, as in the 
   case of
 
   @{ML_matchresult_fake_both [display,gray]
-  "@{thm conjI} RS @{thm mp}" 
-"*** Exception- THM (\"RSN: no unifiers\", 1, 
-[\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}
+  \<open>@{thm conjI} RS @{thm mp}\<close> 
+\<open>*** Exception- THM ("RSN: no unifiers", 1, 
+["\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q", "\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q"]) raised\<close>}
 
   then the function raises an exception. The function @{ML_ind  RSN in Drule} 
   is similar to @{ML RS}, but takes an additional number as argument. This 
@@ -783,8 +783,8 @@
   the function @{ML_ind MRS in Drule}:
 
   @{ML_matchresult_fake [display,gray]
-  "[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}" 
-  "\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)"}
+  \<open>[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}\<close> 
+  \<open>\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)\<close>}
 
   If you need to instantiate lists of theorems, you can use the
   functions @{ML_ind RL in Drule} and @{ML_ind OF in Drule}. For 
@@ -792,16 +792,16 @@
   instantiated with every theorem in the first.
 
   @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val list1 = [@{thm impI}, @{thm disjI2}]
   val list2 = [@{thm conjI}, @{thm disjI1}]
 in
   list1 RL list2
-end" 
-"[\<lbrakk>?P1 \<Longrightarrow> ?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<and> ?Q, 
+end\<close> 
+\<open>[\<lbrakk>?P1 \<Longrightarrow> ?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<and> ?Q, 
  \<lbrakk>?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q,
  (?P1 \<Longrightarrow> ?Q1) \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<or> ?Q, 
- ?Q1 \<Longrightarrow> (?P1 \<or> ?Q1) \<or> ?Q]"}
+ ?Q1 \<Longrightarrow> (?P1 \<or> ?Q1) \<or> ?Q]\<close>}
 
   \begin{readmore}
   The combinators for instantiating theorems with other theorems are 
@@ -981,7 +981,7 @@
   There is even another way of implementing this tactic: in automatic proof
   procedures (in contrast to tactics that might be called by the user) there
   are often long lists of tactics that are applied to the first
-  subgoal. Instead of writing the code above and then calling @{ML "foo_tac'' @{context} 1"}, 
+  subgoal. Instead of writing the code above and then calling @{ML \<open>foo_tac'' @{context} 1\<close>}, 
   you can also just write
 \<close>
 
@@ -1097,7 +1097,7 @@
   convention therefore, tactics visible to the user should either change
   something or fail.
 
-  To comply with this convention, we could simply delete the @{ML "K all_tac"}
+  To comply with this convention, we could simply delete the @{ML \<open>K all_tac\<close>}
   in @{ML select_tac'} or delete @{ML TRY} from @{ML select_tac''}. But for
   the sake of argument, let us suppose that this deletion is \emph{not} an
   option. In such cases, you can use the combinator @{ML_ind CHANGED in
@@ -1459,10 +1459,10 @@
   empty simpset, i.e., @{ML_ind empty_ss in Raw_Simplifier}
   
   @{ML_matchresult_fake [display,gray]
-  "print_ss @{context} empty_ss"
-"Simplification rules:
+  \<open>print_ss @{context} empty_ss\<close>
+\<open>Simplification rules:
 Congruences rules:
-Simproc patterns:"}
+Simproc patterns:\<close>}
 
   you can see it contains nothing. This simpset is usually not useful, except as a 
   building block to build bigger simpsets. For example you can add to @{ML empty_ss} 
@@ -1475,11 +1475,11 @@
   Printing then out the components of the simpset gives:
 
   @{ML_matchresult_fake [display,gray]
-  "print_ss @{context} (Raw_Simplifier.simpset_of ss1)"
-"Simplification rules:
+  \<open>print_ss @{context} (Raw_Simplifier.simpset_of ss1)\<close>
+\<open>Simplification rules:
   ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:
-Simproc patterns:"}
+Simproc patterns:\<close>}
 
   \footnote{\bf FIXME: Why does it print out ??.unknown}
 
@@ -1492,13 +1492,13 @@
   gives
 
   @{ML_matchresult_fake [display,gray]
-  "print_ss @{context} (Raw_Simplifier.simpset_of ss2)"
-"Simplification rules:
+  \<open>print_ss @{context} (Raw_Simplifier.simpset_of ss2)\<close>
+\<open>Simplification rules:
   ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:
   Complete_Lattices.Inf_class.INFIMUM: 
     \<lbrakk>A1 = B1; \<And>x. x \<in> B1 =simp=> C1 x = D1 x\<rbrakk> \<Longrightarrow> INFIMUM A1 C1 \<equiv> INFIMUM B1 D1
-Simproc patterns:"}
+Simproc patterns:\<close>}
 
   Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} 
   expects this form of the simplification and congruence rules. This is
@@ -1509,10 +1509,10 @@
   HOL_basic_ss in Simpdata}. While printing out the components of this simpset
 
   @{ML_matchresult_fake [display,gray]
-  "print_ss @{context} HOL_basic_ss"
-"Simplification rules:
+  \<open>print_ss @{context} HOL_basic_ss\<close>
+\<open>Simplification rules:
 Congruences rules:
-Simproc patterns:"}
+Simproc patterns:\<close>}
 
   also produces ``nothing'', the printout is somewhat misleading. In fact
   the @{ML HOL_basic_ss} is setup so that it can solve goals of the
@@ -1543,8 +1543,8 @@
   connectives in HOL. 
 
   @{ML_matchresult_fake [display,gray]
-  "print_ss @{context} HOL_ss"
-"Simplification rules:
+  \<open>print_ss @{context} HOL_ss\<close>
+\<open>Simplification rules:
   Pure.triv_forall_equality: (\<And>x. PROP V) \<equiv> PROP V
   HOL.the_eq_trivial: THE x. x = y \<equiv> y
   HOL.the_sym_eq_trivial: THE ya. y = ya \<equiv> y
@@ -1554,7 +1554,7 @@
     \<Longrightarrow> (PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')
   op -->: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'
 Simproc patterns:
-  \<dots>"}
+  \<dots>\<close>}
 
   \begin{readmore}
   The simplifier for HOL is set up in @{ML_file "HOL/Tools/simpdata.ML"}.
@@ -1755,7 +1755,7 @@
 
   (FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy)
 
-  (FIXME: explain @{ML simplify} and @{ML "Simplifier.rewrite_rule"} etc.)
+  (FIXME: explain @{ML simplify} and @{ML \<open>Simplifier.rewrite_rule\<close>} etc.)
 
 \<close>
 
@@ -2065,29 +2065,29 @@
   instance of the (meta)reflexivity theorem. For example:
 
   @{ML_matchresult_fake [display,gray]
-  "Conv.all_conv @{cterm \"Foo \<or> Bar\"}"
-  "Foo \<or> Bar \<equiv> Foo \<or> Bar"}
+  \<open>Conv.all_conv @{cterm "Foo \<or> Bar"}\<close>
+  \<open>Foo \<or> Bar \<equiv> Foo \<or> Bar\<close>}
 
   Another simple conversion is @{ML_ind  no_conv in Conv} which always raises the 
   exception @{ML CTERM}.
 
   @{ML_matchresult_fake [display,gray]
-  "Conv.no_conv @{cterm True}" 
-  "*** Exception- CTERM (\"no conversion\", []) raised"}
+  \<open>Conv.no_conv @{cterm True}\<close> 
+  \<open>*** Exception- CTERM ("no conversion", []) raised\<close>}
 
   A more interesting conversion is the function @{ML_ind  beta_conversion in Thm}: it 
   produces a meta-equation between a term and its beta-normal form. For example
 
   @{ML_matchresult_fake [display,gray]
-  "let
-  val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
-  val two = @{cterm \"2::nat\"}
-  val ten = @{cterm \"10::nat\"}
+  \<open>let
+  val add = @{cterm "\<lambda>x y. x + (y::nat)"}
+  val two = @{cterm "2::nat"}
+  val ten = @{cterm "10::nat"}
   val ctrm = Thm.apply (Thm.apply add two) ten
 in
   Thm.beta_conversion true ctrm
-end"
-  "((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"}
+end\<close>
+  \<open>((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10\<close>}
 
   If you run this example, you will notice that the actual response is the 
   seemingly nonsensical @{term
@@ -2097,25 +2097,25 @@
   we obtain the expected result.
 
   @{ML_matchresult [display,gray]
-"let
-  val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
-  val two = @{cterm \"2::nat\"}
-  val ten = @{cterm \"10::nat\"}
+\<open>let
+  val add = @{cterm "\<lambda>x y. x + (y::nat)"}
+  val two = @{cterm "2::nat"}
+  val ten = @{cterm "10::nat"}
   val ctrm = Thm.apply (Thm.apply add two) ten
 in
   Thm.prop_of (Thm.beta_conversion true ctrm)
-end"
-"Const (\"Pure.eq\",_) $ 
-  (Abs (\"x\",_,Abs (\"y\",_,_)) $_$_) $ 
-    (Const (\"Groups.plus_class.plus\",_) $ _ $ _)"} 
+end\<close>
+\<open>Const ("Pure.eq",_) $ 
+  (Abs ("x",_,Abs ("y",_,_)) $_$_) $ 
+    (Const ("Groups.plus_class.plus",_) $ _ $ _)\<close>} 
 
 or in the pretty-printed form
 
   @{ML_matchresult_fake [display,gray]
-"let
-   val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
-   val two = @{cterm \"2::nat\"}
-   val ten = @{cterm \"10::nat\"}
+\<open>let
+   val add = @{cterm "\<lambda>x y. x + (y::nat)"}
+   val two = @{cterm "2::nat"}
+   val ten = @{cterm "10::nat"}
    val ctrm = Thm.apply (Thm.apply add two) ten
    val ctxt = @{context}
      |> Config.put eta_contract false 
@@ -2124,8 +2124,8 @@
   Thm.prop_of (Thm.beta_conversion true ctrm)
   |> pretty_term ctxt
   |> pwriteln
-end"
-"(\<lambda>x y. x + y) 2 10 \<equiv> 2 + 10"}
+end\<close>
+\<open>(\<lambda>x y. x + y) 2 10 \<equiv> 2 + 10\<close>}
 
   The argument @{ML true} in @{ML beta_conversion in Thm} indicates that 
   the right-hand side should be fully beta-normalised. If instead 
@@ -2147,12 +2147,12 @@
   to @{term "Foo \<longrightarrow> Bar"}. The code is as follows.
 
   @{ML_matchresult_fake [display,gray]
-"let 
-  val ctrm = @{cterm \"True \<and> (Foo \<longrightarrow> Bar)\"}
+\<open>let 
+  val ctrm = @{cterm "True \<and> (Foo \<longrightarrow> Bar)"}
 in
   Conv.rewr_conv @{thm true_conj1} ctrm
-end"
-  "True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}
+end\<close>
+  \<open>True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar\<close>}
 
   Note, however, that the function @{ML_ind  rewr_conv in Conv} only rewrites the 
   outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match 
@@ -2166,14 +2166,14 @@
   which applies one conversion after another. For example
 
   @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val conv1 = Thm.beta_conversion false
   val conv2 = Conv.rewr_conv @{thm true_conj1}
-  val ctrm = Thm.apply @{cterm \"\<lambda>x. x \<and> False\"} @{cterm \"True\"}
+  val ctrm = Thm.apply @{cterm "\<lambda>x. x \<and> False"} @{cterm "True"}
 in
   (conv1 then_conv conv2) ctrm
-end"
-  "(\<lambda>x. x \<and> False) True \<equiv> False"}
+end\<close>
+  \<open>(\<lambda>x. x \<and> False) True \<equiv> False\<close>}
 
   where we first beta-reduce the term and then rewrite according to
   @{thm [source] true_conj1}. (When running this example recall the 
@@ -2183,14 +2183,14 @@
   first one, and if it does not apply, tries the second. For example 
 
   @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv
-  val ctrm1 = @{cterm \"True \<and> Q\"}
-  val ctrm2 = @{cterm \"P \<or> (True \<and> Q)\"}
+  val ctrm1 = @{cterm "True \<and> Q"}
+  val ctrm2 = @{cterm "P \<or> (True \<and> Q)"}
 in
   (conv ctrm1, conv ctrm2)
-end"
-"(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)"}
+end\<close>
+\<open>(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)\<close>}
 
   Here the conversion @{thm [source] true_conj1} only applies
   in the first case, but fails in the second. The whole conversion
@@ -2200,13 +2200,13 @@
   For example
   
   @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1})
-  val ctrm = @{cterm \"True \<or> P\"}
+  val ctrm = @{cterm "True \<or> P"}
 in
   conv ctrm
-end"
-  "True \<or> P \<equiv> True \<or> P"}
+end\<close>
+  \<open>True \<or> P \<equiv> True \<or> P\<close>}
 
   Rewriting with more than one theorem can be done using the function 
   @{ML_ind rewrs_conv in Conv} from the structure @{ML_structure Conv}.
@@ -2221,13 +2221,13 @@
   For example
 
   @{ML_matchresult_fake [display,gray]
-"let 
+\<open>let 
   val conv = Conv.arg_conv (Conv.rewr_conv @{thm true_conj1})
-  val ctrm = @{cterm \"P \<or> (True \<and> Q)\"}
+  val ctrm = @{cterm "P \<or> (True \<and> Q)"}
 in
   conv ctrm
-end"
-"P \<or> (True \<and> Q) \<equiv> P \<or> Q"}
+end\<close>
+\<open>P \<or> (True \<and> Q) \<equiv> P \<or> Q\<close>}
 
   The reason for this behaviour is that \<open>(op \<or>)\<close> expects two
   arguments.  Therefore the term must be of the form \<open>(Const \<dots> $ t1) $ t2\<close>. The
@@ -2239,13 +2239,13 @@
   abstraction. For example:
 
   @{ML_matchresult_fake [display,gray]
-"let 
+\<open>let 
   val conv = Conv.rewr_conv @{thm true_conj1} 
-  val ctrm = @{cterm \"\<lambda>P. True \<and> (P \<and> Foo)\"}
+  val ctrm = @{cterm "\<lambda>P. True \<and> (P \<and> Foo)"}
 in
   Conv.abs_conv (K conv) @{context} ctrm
-end"
-  "\<lambda>P. True \<and> (P \<and> Foo) \<equiv> \<lambda>P. P \<and> Foo"}
+end\<close>
+  \<open>\<lambda>P. True \<and> (P \<and> Foo) \<equiv> \<lambda>P. P \<and> Foo\<close>}
   
   Note that this conversion needs a context as an argument. We also give the
   conversion as \<open>(K conv)\<close>, which is a function that ignores its
@@ -2280,13 +2280,13 @@
   conversion in action, consider the following example:
 
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val conv = true_conj1_conv @{context}
-  val ctrm = @{cterm \"distinct [1::nat, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}
+  val ctrm = @{cterm "distinct [1::nat, x] \<longrightarrow> True \<and> 1 \<noteq> x"}
 in
   conv ctrm
-end"
-  "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
+end\<close>
+  \<open>distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x\<close>}
 \<close>
 
 text \<open>
@@ -2323,17 +2323,17 @@
   two results are calculated. 
 
   @{ML_matchresult_fake [display, gray]
-  "let
+  \<open>let
   val ctxt = @{context}
   val conv = Conv.try_conv (Conv.rewrs_conv @{thms conj_assoc})
   val conv_top = Conv.top_conv (K conv) ctxt
   val conv_bot = Conv.bottom_conv (K conv) ctxt
-  val ctrm = @{cterm \"(a \<and> (b \<and> c)) \<and> d\"}
+  val ctrm = @{cterm "(a \<and> (b \<and> c)) \<and> d"}
 in
   (conv_top ctrm, conv_bot ctrm)
-end"
-  "(\"(a \<and> (b \<and> c)) \<and> d \<equiv> a \<and> (b \<and> (c \<and> d))\",
- \"(a \<and> (b \<and> c)) \<and> d \<equiv> (a \<and> b) \<and> (c \<and> d)\")"}
+end\<close>
+  \<open>("(a \<and> (b \<and> c)) \<and> d \<equiv> a \<and> (b \<and> (c \<and> d))",
+ "(a \<and> (b \<and> c)) \<and> d \<equiv> (a \<and> b) \<and> (c \<and> d)")\<close>}
 
   To see how much control you have over rewriting with conversions, let us 
   make the task a bit more complicated by rewriting according to the rule
@@ -2359,14 +2359,14 @@
 
 
   @{ML_matchresult_fake [display,gray]
-"let
-  val ctrm = @{cterm \"if P (True \<and> 1 \<noteq> (2::nat)) 
-                        then True \<and> True else True \<and> False\"}
+\<open>let
+  val ctrm = @{cterm "if P (True \<and> 1 \<noteq> (2::nat)) 
+                        then True \<and> True else True \<and> False"}
 in
   if_true1_conv @{context} ctrm
-end"
-"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False 
-\<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"}
+end\<close>
+\<open>if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False 
+\<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False\<close>}
 \<close>
 
 text \<open>
@@ -2383,13 +2383,13 @@
   new theorem as follows
 
   @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val conv = Conv.fconv_rule (true_conj1_conv @{context}) 
   val thm = @{thm foo_test}
 in
   conv thm
-end" 
-  "?P \<or> \<not> ?P"}
+end\<close> 
+  \<open>?P \<or> \<not> ?P\<close>}
 
   Finally, Isabelle provides function @{ML_ind CONVERSION in Tactical} 
   for turning conversions into tactics. This needs some predefined conversion 
@@ -2420,7 +2420,7 @@
           Conv.concl_conv ~1 (true_conj1_conv ctxt))) ctxt)\<close>
 
 text \<open>
-  We call the conversions with the argument @{ML "~1"}. By this we 
+  We call the conversions with the argument @{ML \<open>~1\<close>}. By this we 
   analyse all parameters, all premises and the conclusion of a goal
   state. If we call @{ML concl_conv in Conv} with 
   a non-negative number, say \<open>n\<close>, then this conversions will 
@@ -2466,8 +2466,8 @@
   left-hand side in the right-hand side.
 
   @{ML_matchresult_fake [display,gray]
-  "Drule.abs_def @{thm id1_def}"
-  "id1 \<equiv> \<lambda>x. x"}
+  \<open>Drule.abs_def @{thm id1_def}\<close>
+  \<open>id1 \<equiv> \<lambda>x. x\<close>}
 
   Unfortunately, Isabelle has no built-in function that transforms the
   theorems in the other direction. We can implement one using
@@ -2514,8 +2514,8 @@
   produce meta-variables for the theorem.  An example is as follows.
 
   @{ML_matchresult_fake [display, gray]
-  "unabs_def @{context} @{thm id2_def}"
-  "id2 ?x1 \<equiv> ?x1"}
+  \<open>unabs_def @{context} @{thm id2_def}\<close>
+  \<open>id2 ?x1 \<equiv> ?x1\<close>}
 \<close>
 
 text \<open>