diff -r cf7f3465eaf1 -r 240563fbf41d src/ZF/Induct/Term.thy
--- a/src/ZF/Induct/Term.thy	Thu Jul 23 14:20:51 2015 +0200
+++ b/src/ZF/Induct/Term.thy	Thu Jul 23 14:25:05 2015 +0200
@@ -3,14 +3,14 @@
     Copyright   1994  University of Cambridge
 *)
 
-section {* Terms over an alphabet *}
+section \<open>Terms over an alphabet\<close>
 
 theory Term imports Main begin
 
-text {*
+text \<open>
   Illustrates the list functor (essentially the same type as in @{text
   Trees_Forest}).
-*}
+\<close>
 
 consts
   "term" :: "i => i"
@@ -56,7 +56,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)"
-  -- {* Induction on @{term "term(A)"} followed by induction on @{term list}. *}
+  -- \<open>Induction on @{term "term(A)"} followed by induction on @{term list}.\<close>
   apply (induct_tac t)
   apply (erule list.induct)
    apply (auto dest: list_CollectD)
@@ -67,15 +67,15 @@
       !!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)"
-  -- {* Induction on @{term "term(A)"} to prove an equation. *}
+  -- \<open>Induction on @{term "term(A)"} to prove an equation.\<close>
   apply (induct_tac t)
   apply (auto dest: map_list_Collect list_CollectD)
   done
 
-text {*
+text \<open>
   \medskip Lemmas to justify using @{term "term"} in other recursive
   type definitions.
-*}
+\<close>
 
 lemma term_mono: "A \<subseteq> B ==> term(A) \<subseteq> term(B)"
   apply (unfold term.defs)
@@ -85,7 +85,7 @@
   done
 
 lemma term_univ: "term(univ(A)) \<subseteq> univ(A)"
-  -- {* Easily provable by induction also *}
+  -- \<open>Easily provable by induction also\<close>
   apply (unfold term.defs term.con_defs)
   apply (rule lfp_lowerbound)
    apply (rule_tac [2] A_subset_univ [THEN univ_mono])
@@ -102,13 +102,13 @@
 lemma term_into_univ: "[| t \<in> term(A);  A \<subseteq> univ(B) |] ==> t \<in> univ(B)"
   by (rule term_subset_univ [THEN subsetD])
 
-text {*
+text \<open>
   \medskip @{text term_rec} -- by @{text Vset} recursion.
-*}
+\<close>
 
 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)"
-  -- {* @{term map} works correctly on the underlying list of terms. *}
+  -- \<open>@{term map} works correctly on the underlying list of terms.\<close>
   apply (induct set: list)
    apply simp
   apply (subgoal_tac "rank (a) <i & rank (l) < i")
@@ -119,7 +119,7 @@
 
 lemma term_rec [simp]: "ts \<in> list(A) ==>
   term_rec(Apply(a,ts), d) = d(a, ts, map (\<lambda>z. term_rec(z,d), ts))"
-  -- {* Typing premise is necessary to invoke @{text map_lemma}. *}
+  -- \<open>Typing premise is necessary to invoke @{text map_lemma}.\<close>
   apply (rule term_rec_def [THEN def_Vrec, THEN trans])
   apply (unfold term.con_defs)
   apply (simp add: rank_pair2 map_lemma)
@@ -131,7 +131,7 @@
                    r \<in> list(\<Union>t \<in> term(A). C(t)) |]
                 ==> d(x, zs, r): C(Apply(x,zs))"
   shows "term_rec(t,d) \<in> C(t)"
-  -- {* Slightly odd typing condition on @{text r} in the second premise! *}
+  -- \<open>Slightly odd typing condition on @{text r} in the second premise!\<close>
   using t
   apply induct
   apply (frule list_CollectD)
@@ -159,9 +159,9 @@
   done
 
 
-text {*
+text \<open>
   \medskip @{term term_map}.
-*}
+\<close>
 
 lemma term_map [simp]:
   "ts \<in> list(A) ==>
@@ -181,9 +181,9 @@
   apply (erule RepFunI)
   done
 
-text {*
+text \<open>
   \medskip @{term term_size}.
-*}
+\<close>
 
 lemma term_size [simp]:
     "ts \<in> list(A) ==> term_size(Apply(a, ts)) = succ(list_add(map(term_size, ts)))"
@@ -193,9 +193,9 @@
   by (auto simp add: term_size_def)
 
 
-text {*
+text \<open>
   \medskip @{text reflect}.
-*}
+\<close>
 
 lemma reflect [simp]:
     "ts \<in> list(A) ==> reflect(Apply(a, ts)) = Apply(a, rev(map(reflect, ts)))"
@@ -205,9 +205,9 @@
   by (auto simp add: reflect_def)
 
 
-text {*
+text \<open>
   \medskip @{text preorder}.
-*}
+\<close>
 
 lemma preorder [simp]:
     "ts \<in> list(A) ==> preorder(Apply(a, ts)) = Cons(a, flat(map(preorder, ts)))"
@@ -217,9 +217,9 @@
   by (simp add: preorder_def)
 
 
-text {*
+text \<open>
   \medskip @{text postorder}.
-*}
+\<close>
 
 lemma postorder [simp]:
     "ts \<in> list(A) ==> postorder(Apply(a, ts)) = flat(map(postorder, ts)) @ [a]"
@@ -229,9 +229,9 @@
   by (simp add: postorder_def)
 
 
-text {*
+text \<open>
   \medskip Theorems about @{text term_map}.
-*}
+\<close>
 
 declare map_compose [simp]
 
@@ -247,9 +247,9 @@
   by (induct rule: term_induct_eqn) (simp add: rev_map_distrib [symmetric])
 
 
-text {*
+text \<open>
   \medskip Theorems about @{text term_size}.
-*}
+\<close>
 
 lemma term_size_term_map: "t \<in> term(A) ==> term_size(term_map(f,t)) = term_size(t)"
   by (induct rule: term_induct_eqn) simp
@@ -261,17 +261,17 @@
   by (induct rule: term_induct_eqn) (simp add: length_flat)
 
 
-text {*
+text \<open>
   \medskip Theorems about @{text reflect}.
-*}
+\<close>
 
 lemma reflect_reflect_ident: "t \<in> term(A) ==> reflect(reflect(t)) = t"
   by (induct rule: term_induct_eqn) (simp add: rev_map_distrib)
 
 
-text {*
+text \<open>
   \medskip Theorems about preorder.
-*}
+\<close>
 
 lemma preorder_term_map:
     "t \<in> term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))"