src/ZF/Induct/Term.thy

--- a/src/ZF/Induct/Term.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/ZF/Induct/Term.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -55,7 +55,7 @@
       !!x z zs. [| x \<in> A;  z \<in> term(A);  zs: list(term(A));  P(Apply(x,zs))
                 |] ==> P(Apply(x, Cons(z,zs)))
      |] ==> P(t)"
-  \<comment> \<open>Induction on @{term "term(A)"} followed by induction on @{term list}.\<close>
+  \<comment> \<open>Induction on \<^term>\<open>term(A)\<close> followed by induction on \<^term>\<open>list\<close>.\<close>
   apply (induct_tac t)
   apply (erule list.induct)
    apply (auto dest: list_CollectD)
@@ -66,13 +66,13 @@
       !!x zs. [| x \<in> A;  zs: list(term(A));  map(f,zs) = map(g,zs) |] ==>
               f(Apply(x,zs)) = g(Apply(x,zs))
    |] ==> f(t) = g(t)"
-  \<comment> \<open>Induction on @{term "term(A)"} to prove an equation.\<close>
+  \<comment> \<open>Induction on \<^term>\<open>term(A)\<close> to prove an equation.\<close>
   apply (induct_tac t)
   apply (auto dest: map_list_Collect list_CollectD)
   done
 
 text \<open>
-  \medskip Lemmas to justify using @{term "term"} in other recursive
+  \medskip Lemmas to justify using \<^term>\<open>term\<close> in other recursive
   type definitions.
 \<close>
 
@@ -107,7 +107,7 @@
 
 lemma map_lemma: "[| l \<in> list(A);  Ord(i);  rank(l)<i |]
     ==> map(\<lambda>z. (\<lambda>x \<in> Vset(i).h(x)) ` z, l) = map(h,l)"
-  \<comment> \<open>@{term map} works correctly on the underlying list of terms.\<close>
+  \<comment> \<open>\<^term>\<open>map\<close> works correctly on the underlying list of terms.\<close>
   apply (induct set: list)
    apply simp
   apply (subgoal_tac "rank (a) <i & rank (l) < i")
@@ -159,7 +159,7 @@
 
 
 text \<open>
-  \medskip @{term term_map}.
+  \medskip \<^term>\<open>term_map\<close>.
 \<close>
 
 lemma term_map [simp]:
@@ -181,7 +181,7 @@
   done
 
 text \<open>
-  \medskip @{term term_size}.
+  \medskip \<^term>\<open>term_size\<close>.
 \<close>
 
 lemma term_size [simp]: