# HG changeset patch
# User wenzelm
# Date 1451321010 -3600
# Node ID 546958347e05401aa82a8ff5f9d1bcc2e8113f18
# Parent  cbd310584cff6266be8f0a9135ff7c1821dbd10b
prefer symbols for "Union", "Inter";

diff -r cbd310584cff -r 546958347e05 src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Algebra/Ideal.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -47,7 +47,7 @@
 subsubsection (in ring) \<open>Ideals Generated by a Subset of @{term "carrier R"}\<close>
 
 definition genideal :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set"  ("Idl\<index> _" [80] 79)
-  where "genideal R S = Inter {I. ideal I R \<and> S \<subseteq> I}"
+  where "genideal R S = \<Inter>{I. ideal I R \<and> S \<subseteq> I}"
 
 subsubsection \<open>Principal Ideals\<close>
 
@@ -218,7 +218,7 @@
 lemma (in ring) i_Intersect:
   assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R"
     and notempty: "S \<noteq> {}"
-  shows "ideal (Inter S) R"
+  shows "ideal (\<Inter>S) R"
   apply (unfold_locales)
   apply (simp_all add: Inter_eq)
         apply rule unfolding mem_Collect_eq defer 1
diff -r cbd310584cff -r 546958347e05 src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -785,9 +785,9 @@
 lemma Card_order_lists: "Card_order r \<Longrightarrow> r \<le>o |lists(Field r) |"
 using card_of_lists card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
 
-lemma Union_set_lists:
-"Union(set ` (lists A)) = A"
-unfolding lists_def2 proof(auto)
+lemma Union_set_lists: "\<Union>(set ` (lists A)) = A"
+  unfolding lists_def2
+proof(auto)
   fix a assume "a \<in> A"
   hence "set [a] \<le> A \<and> a \<in> set [a]" by auto
   thus "\<exists>l. set l \<le> A \<and> a \<in> set l" by blast
diff -r cbd310584cff -r 546958347e05 src/HOL/Cardinals/Wellorder_Relation.thy
--- a/src/HOL/Cardinals/Wellorder_Relation.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -441,15 +441,15 @@
 unfolding ofilter_def by blast
 
 lemma ofilter_Inter:
-"\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> ofilter A\<rbrakk> \<Longrightarrow> ofilter (Inter S)"
+"\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> ofilter A\<rbrakk> \<Longrightarrow> ofilter (\<Inter>S)"
 unfolding ofilter_def by blast
 
 lemma ofilter_Union:
-"(\<And> A. A \<in> S \<Longrightarrow> ofilter A) \<Longrightarrow> ofilter (Union S)"
+"(\<And> A. A \<in> S \<Longrightarrow> ofilter A) \<Longrightarrow> ofilter (\<Union>S)"
 unfolding ofilter_def by blast
 
 lemma ofilter_under_Union:
-"ofilter A \<Longrightarrow> A = Union {under a| a. a \<in> A}"
+"ofilter A \<Longrightarrow> A = \<Union>{under a| a. a \<in> A}"
 using ofilter_under_UNION[of A]
 by(unfold Union_eq, auto)
 
diff -r cbd310584cff -r 546958347e05 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Complete_Lattices.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -901,12 +901,9 @@
 
 subsubsection \<open>Inter\<close>
 
-abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
-  "Inter S \<equiv> \<Sqinter>S"
+abbreviation Inter :: "'a set set \<Rightarrow> 'a set"  ("\<Inter>_" [900] 900)
+  where "\<Inter>S \<equiv> \<Sqinter>S"
   
-notation (xsymbols)
-  Inter  ("\<Inter>_" [900] 900)
-
 lemma Inter_eq:
   "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
 proof (rule set_eqI)
@@ -944,7 +941,7 @@
   "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B"
   by (fact Inf_less_eq)
 
-lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> Inter A"
+lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> \<Inter>A"
   by (fact Inf_greatest)
 
 lemma Inter_empty: "\<Inter>{} = UNIV"
@@ -1080,11 +1077,8 @@
 
 subsubsection \<open>Union\<close>
 
-abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
-  "Union S \<equiv> \<Squnion>S"
-
-notation (xsymbols)
-  Union  ("\<Union>_" [900] 900)
+abbreviation Union :: "'a set set \<Rightarrow> 'a set"  ("\<Union>_" [900] 900)
+  where "\<Union>S \<equiv> \<Squnion>S"
 
 lemma Union_eq:
   "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
diff -r cbd310584cff -r 546958347e05 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Equiv_Relations.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -108,7 +108,7 @@
   "X \<in> A//r ==> (!!x. X = r``{x} ==> x \<in> A ==> P) ==> P"
   by (unfold quotient_def) blast
 
-lemma Union_quotient: "equiv A r ==> Union (A//r) = A"
+lemma Union_quotient: "equiv A r ==> \<Union>(A//r) = A"
   by (unfold equiv_def refl_on_def quotient_def) blast
 
 lemma quotient_disj:
diff -r cbd310584cff -r 546958347e05 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Groups_Big.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -172,7 +172,7 @@
 
 lemma Union_disjoint:
   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
-  shows "F g (Union C) = (F \<circ> F) g C"
+  shows "F g (\<Union>C) = (F \<circ> F) g C"
 proof cases
   assume "finite C"
   from UNION_disjoint [OF this assms]
@@ -994,7 +994,7 @@
 lemma card_Union_disjoint:
   "finite C ==> (ALL A:C. finite A) ==>
    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
-   ==> card (Union C) = setsum card C"
+   ==> card (\<Union>C) = setsum card C"
 apply (frule card_UN_disjoint [of C id])
 apply simp_all
 done
diff -r cbd310584cff -r 546958347e05 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Inductive.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -87,16 +87,16 @@
 
 lemma lfp_induct_set:
   assumes lfp: "a: lfp(f)"
-      and mono: "mono(f)"
-      and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
+    and mono: "mono(f)"
+    and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
   shows "P(a)"
   by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
      (auto simp: intro: indhyp)
 
 lemma lfp_ordinal_induct_set: 
   assumes mono: "mono f"
-  and P_f: "!!S. P S ==> P(f S)"
-  and P_Union: "!!M. !S:M. P S ==> P(Union M)"
+    and P_f: "!!S. P S ==> P(f S)"
+    and P_Union: "!!M. !S:M. P S ==> P (\<Union>M)"
   shows "P(lfp f)"
   using assms by (rule lfp_ordinal_induct)
 
diff -r cbd310584cff -r 546958347e05 src/HOL/Library/Countable_Set_Type.thy
--- a/src/HOL/Library/Countable_Set_Type.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -118,7 +118,7 @@
   is "UNION" parametric UNION_transfer by simp
 definition cUnion :: "'a cset cset \<Rightarrow> 'a cset" where "cUnion A = cUNION A id"
 
-lemma Union_conv_UNION: "Union A = UNION A id"
+lemma Union_conv_UNION: "\<Union>A = UNION A id"
 by auto
 
 lemma cUnion_transfer [transfer_rule]:
diff -r cbd310584cff -r 546958347e05 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Library/FSet.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -79,7 +79,7 @@
 lemma right_total_Inf_fset_transfer:
   assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
   shows "(rel_set (rel_set A) ===> rel_set A) 
-    (\<lambda>S. if finite (Inter S \<inter> Collect (Domainp A)) then Inter S \<inter> Collect (Domainp A) else {}) 
+    (\<lambda>S. if finite (\<Inter>S \<inter> Collect (Domainp A)) then \<Inter>S \<inter> Collect (Domainp A) else {}) 
       (\<lambda>S. if finite (Inf S) then Inf S else {})"
     by transfer_prover
 
diff -r cbd310584cff -r 546958347e05 src/HOL/Library/Old_Datatype.thy
--- a/src/HOL/Library/Old_Datatype.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Library/Old_Datatype.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -76,7 +76,7 @@
   In1_def:    "In1(M) == Scons (Numb 1) M"
 
   (*Function spaces*)
-  Lim_def: "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}"
+  Lim_def: "Lim f == \<Union>{z. ? x. z = Push_Node (Inl x) ` (f x)}"
 
   (*the set of nodes with depth less than k*)
   ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
diff -r cbd310584cff -r 546958347e05 src/HOL/Lifting_Set.thy
--- a/src/HOL/Lifting_Set.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Lifting_Set.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -237,7 +237,7 @@
 
 lemma right_total_Inter_transfer [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
-  shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>S. Inter S \<inter> Collect (Domainp A)) Inter"
+  shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>S. \<Inter>S \<inter> Collect (Domainp A)) Inter"
   unfolding Inter_eq[abs_def]
   by (subst Collect_conj_eq[symmetric]) transfer_prover
 
diff -r cbd310584cff -r 546958347e05 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -424,7 +424,7 @@
     apply (case_tac "\<not> stable r step ss p")
     apply simp_all
     done
-  also have "\<And>f. (UN p:{..<size ss}. f p) = Union (set (map f [0..<size ss]))" by auto
+  also have "\<And>f. (UN p:{..<size ss}. f p) = \<Union>(set (map f [0..<size ss]))" by auto
   also note Sup_set_fold also note fold_map
   also have "op \<union> \<circ> (\<lambda>p. if \<not> stable r step ss p then {p} else {}) = 
             (\<lambda>p A. if \<not>stable r step ss p then insert p A else A)"
diff -r cbd310584cff -r 546958347e05 src/HOL/MicroJava/BV/JVMType.thy
--- a/src/HOL/MicroJava/BV/JVMType.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -62,7 +62,7 @@
                    
 
 lemma JVM_states_unfold: 
-  "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) \<times>
+  "states S maxs maxr == err(opt((\<Union>{list n (types S) |n. n <= maxs}) \<times>
                                   list maxr (err(types S))))"
   apply (unfold states_def sl_def Opt.esl_def Err.sl_def
          stk_esl_def reg_sl_def Product.esl_def
diff -r cbd310584cff -r 546958347e05 src/HOL/MicroJava/DFA/Err.thy
--- a/src/HOL/MicroJava/DFA/Err.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/MicroJava/DFA/Err.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -283,7 +283,7 @@
   done 
 qed
 
-subsection \<open>semilat (err(Union AS))\<close>
+subsection \<open>semilat (err (Union AS))\<close>
 
 (* FIXME? *)
 lemma all_bex_swap_lemma [iff]:
@@ -293,7 +293,7 @@
 lemma closed_err_Union_lift2I: 
   "\<lbrakk> !A:AS. closed (err A) (lift2 f); AS ~= {}; 
       !A:AS.!B:AS. A~=B \<longrightarrow> (!a:A.!b:B. a +_f b = Err) \<rbrakk> 
-  \<Longrightarrow> closed (err(Union AS)) (lift2 f)"
+  \<Longrightarrow> closed (err (\<Union>AS)) (lift2 f)"
 apply (unfold closed_def err_def)
 apply simp
 apply clarify
@@ -309,7 +309,7 @@
 lemma err_semilat_UnionI:
   "\<lbrakk> !A:AS. err_semilat(A, r, f); AS ~= {}; 
       !A:AS.!B:AS. A~=B \<longrightarrow> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) \<rbrakk> 
-  \<Longrightarrow> err_semilat(Union AS, r, f)"
+  \<Longrightarrow> err_semilat (\<Union>AS, r, f)"
 apply (unfold semilat_def sl_def)
 apply (simp add: closed_err_Union_lift2I)
 apply (rule conjI)
diff -r cbd310584cff -r 546958347e05 src/HOL/MicroJava/DFA/Listn.thy
--- a/src/HOL/MicroJava/DFA/Listn.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/MicroJava/DFA/Listn.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -44,7 +44,7 @@
 "sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err"
 
 definition upto_esl :: "nat \<Rightarrow> 'a esl \<Rightarrow> 'a list esl" where
-"upto_esl m == %(A,r,f). (Union{list n A |n. n <= m}, le r, sup f)"
+"upto_esl m == %(A,r,f). (\<Union>{list n A |n. n <= m}, le r, sup f)"
 
 lemmas [simp] = set_update_subsetI
 
diff -r cbd310584cff -r 546958347e05 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -74,7 +74,7 @@
   finally show ?thesis .
 qed
 
-lemma subspace_Inter: "\<forall>s \<in> f. subspace s \<Longrightarrow> subspace (Inter f)"
+lemma subspace_Inter: "\<forall>s \<in> f. subspace s \<Longrightarrow> subspace (\<Inter>f)"
   unfolding subspace_def by auto
 
 lemma span_eq[simp]: "span s = s \<longleftrightarrow> subspace s"
@@ -1110,7 +1110,7 @@
 lemma cone_0: "cone {0}"
   unfolding cone_def by auto
 
-lemma cone_Union[intro]: "(\<forall>s\<in>f. cone s) \<longrightarrow> cone (Union f)"
+lemma cone_Union[intro]: "(\<forall>s\<in>f. cone s) \<longrightarrow> cone (\<Union>f)"
   unfolding cone_def by blast
 
 lemma cone_iff:
@@ -8075,7 +8075,7 @@
       assume z: "z \<in> \<Inter>{rel_interior S |S. S \<in> I}"
       {
         fix x
-        assume x: "x \<in> Inter I"
+        assume x: "x \<in> \<Inter>I"
         {
           fix S
           assume S: "S \<in> I"
diff -r cbd310584cff -r 546958347e05 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -203,13 +203,13 @@
 
 lemma open_countable_basis_ex:
   assumes "open X"
-  shows "\<exists>B' \<subseteq> B. X = Union B'"
+  shows "\<exists>B' \<subseteq> B. X = \<Union>B'"
   using assms countable_basis is_basis
   unfolding topological_basis_def by blast
 
 lemma open_countable_basisE:
   assumes "open X"
-  obtains B' where "B' \<subseteq> B" "X = Union B'"
+  obtains B' where "B' \<subseteq> B" "X = \<Union>B'"
   using assms open_countable_basis_ex
   by (atomize_elim) simp
 
@@ -1885,7 +1885,7 @@
 lemma connected_component_of_subset: "\<lbrakk>connected_component s x y; s \<subseteq> t\<rbrakk> \<Longrightarrow> connected_component t x y"
   by (auto simp: connected_component_def)
 
-lemma connected_component_Union: "connected_component_set s x = Union {t. connected t \<and> x \<in> t \<and> t \<subseteq> s}"
+lemma connected_component_Union: "connected_component_set s x = \<Union>{t. connected t \<and> x \<in> t \<and> t \<subseteq> s}"
   by (auto simp: connected_component_def)
 
 lemma connected_connected_component [iff]: "connected (connected_component_set s x)"
@@ -2024,7 +2024,7 @@
 by (metis (no_types, hide_lams) connected_component_eq_eq connected_component_in connected_component_maximal subsetD mem_Collect_eq)
 
 
-lemma Union_connected_component: "Union (connected_component_set s ` s) = s"
+lemma Union_connected_component: "\<Union>(connected_component_set s ` s) = s"
   apply (rule subset_antisym)
   apply (simp add: SUP_least connected_component_subset)
   using connected_component_refl_eq
@@ -2033,7 +2033,7 @@
 
 lemma complement_connected_component_unions:
     "s - connected_component_set s x =
-     Union (connected_component_set s ` s - {connected_component_set s x})"
+     \<Union>(connected_component_set s ` s - {connected_component_set s x})"
   apply (subst Union_connected_component [symmetric], auto)
   apply (metis connected_component_eq_eq connected_component_in)
   by (metis connected_component_eq mem_Collect_eq)
@@ -2053,7 +2053,7 @@
 lemma components_iff: "s \<in> components u \<longleftrightarrow> (\<exists>x. x \<in> u \<and> s = connected_component_set u x)"
   by (auto simp: components_def)
 
-lemma Union_components: "u = Union (components u)"
+lemma Union_components: "u = \<Union>(components u)"
   apply (rule subset_antisym)
   apply (metis Union_connected_component components_def set_eq_subset)
   using Union_connected_component components_def by fastforce
@@ -2142,7 +2142,7 @@
   apply (auto simp: components_iff)
   by (metis connected_component_eq_empty connected_component_intermediate_subset)
 
-lemma in_components_unions_complement: "c \<in> components s \<Longrightarrow> s - c = Union(components s - {c})"
+lemma in_components_unions_complement: "c \<in> components s \<Longrightarrow> s - c = \<Union>(components s - {c})"
   by (metis complement_connected_component_unions components_def components_iff)
 
 lemma connected_intermediate_closure:
diff -r cbd310584cff -r 546958347e05 src/HOL/Number_Theory/MiscAlgebra.thy
--- a/src/HOL/Number_Theory/MiscAlgebra.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -257,7 +257,7 @@
 lemma (in comm_monoid) finprod_Union_disjoint:
   "[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G));
       (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
-   ==> finprod G f (Union C) = finprod G (finprod G f) C"
+   ==> finprod G f (\<Union>C) = finprod G (finprod G f) C"
   apply (frule finprod_UN_disjoint [of C id f])
   apply (auto simp add: SUP_def)
   done
diff -r cbd310584cff -r 546958347e05 src/HOL/Old_Number_Theory/Euler.thy
--- a/src/HOL/Old_Number_Theory/Euler.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Old_Number_Theory/Euler.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -49,7 +49,7 @@
   by (auto simp add: MultInvPair_prop1b)
 
 lemma MultInvPair_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> 
-                          Union ( SetS a p) = SRStar p"
+                          \<Union>(SetS a p) = SRStar p"
   apply (auto simp add: SetS_def MultInvPair_def StandardRes_SRStar_prop4 
     SRStar_mult_prop2)
   apply (frule StandardRes_SRStar_prop3)
@@ -105,7 +105,7 @@
   apply (rule MultInvPair_card_two, auto)
   done
 
-lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))"
+lemma Union_SetS_finite: "2 < p ==> finite (\<Union>(SetS a p))"
   by (auto simp add: SetS_finite SetS_elems_finite)
 
 lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set); 
@@ -118,7 +118,7 @@
 proof -
   have "(p - 1) = 2 * int(card(SetS a p))"
   proof -
-    have "p - 1 = int(card(Union (SetS a p)))"
+    have "p - 1 = int(card(\<Union>(SetS a p)))"
       by (auto simp add: assms MultInvPair_prop2 SRStar_card)
     also have "... = int (setsum card (SetS a p))"
       by (auto simp add: assms SetS_finite SetS_elems_finite
@@ -177,9 +177,9 @@
 lemma Union_SetS_setprod_prop1:
   assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and
     "~(QuadRes p a)"
-  shows "[\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
+  shows "[\<Prod>(\<Union>(SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
 proof -
-  from assms have "[\<Prod>(Union (SetS a p)) = setprod (setprod (%x. x)) (SetS a p)] (mod p)"
+  from assms have "[\<Prod>(\<Union>(SetS a p)) = setprod (setprod (%x. x)) (SetS a p)] (mod p)"
     by (auto simp add: SetS_finite SetS_elems_finite
       MultInvPair_prop1c setprod.Union_disjoint)
   also have "[setprod (setprod (%x. x)) (SetS a p) = 
@@ -199,9 +199,9 @@
 
 lemma Union_SetS_setprod_prop2:
   assumes "zprime p" and "2 < p" and "~([a = 0](mod p))"
-  shows "\<Prod>(Union (SetS a p)) = zfact (p - 1)"
+  shows "\<Prod>(\<Union>(SetS a p)) = zfact (p - 1)"
 proof -
-  from assms have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)"
+  from assms have "\<Prod>(\<Union>(SetS a p)) = \<Prod>(SRStar p)"
     by (auto simp add: MultInvPair_prop2)
   also have "... = \<Prod>({1} \<union> (d22set (p - 1)))"
     by (auto simp add: assms SRStar_d22set_prop)
diff -r cbd310584cff -r 546958347e05 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -75,7 +75,7 @@
   assumes Un [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M"
 
 lemma (in ring_of_sets) finite_Union [intro]:
-  "finite X \<Longrightarrow> X \<subseteq> M \<Longrightarrow> Union X \<in> M"
+  "finite X \<Longrightarrow> X \<subseteq> M \<Longrightarrow> \<Union>X \<in> M"
   by (induct set: finite) (auto simp add: Un)
 
 lemma (in ring_of_sets) finite_UN[intro]:
@@ -261,7 +261,7 @@
 qed
 
 lemma (in sigma_algebra) countable_Union [intro]:
-  assumes "countable X" "X \<subseteq> M" shows "Union X \<in> M"
+  assumes "countable X" "X \<subseteq> M" shows "\<Union>X \<in> M"
 proof cases
   assume "X \<noteq> {}"
   hence "\<Union>X = (\<Union>n. from_nat_into X n)"
diff -r cbd310584cff -r 546958347e05 src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
--- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -105,7 +105,7 @@
 
 primrec used :: "event list => msg set"
 where
-  used_Nil:   "used []         = Union (parts ` initState ` agents)"
+  used_Nil:   "used []         = \<Union>(parts ` initState ` agents)"
 | used_Cons:  "used (ev # evs) =
                      (case ev of
                         Says A B X => parts {X} \<union> used evs
@@ -172,13 +172,13 @@
 
 lemma [code]:
   "analz H = (let
-     H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
+     H' = H \<union> (\<Union>((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
    in if H' = H then H else analz H')"
 sorry
 
 lemma [code]:
   "parts H = (let
-     H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
+     H' = H \<union> (\<Union>((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
    in if H' = H then H else parts H')"
 sorry
 
diff -r cbd310584cff -r 546958347e05 src/HOL/UNITY/ELT.thy
--- a/src/HOL/UNITY/ELT.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/UNITY/ELT.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -133,7 +133,7 @@
 
 (*The Union introduction rule as we should have liked to state it*)
 lemma leadsETo_Union:
-    "(!!A. A : S ==> F : A leadsTo[CC] B) ==> F : (Union S) leadsTo[CC] B"
+    "(!!A. A : S ==> F : A leadsTo[CC] B) ==> F : (\<Union>S) leadsTo[CC] B"
 apply (unfold leadsETo_def)
 apply (blast intro: elt.Union)
 done
@@ -151,7 +151,7 @@
       !!A B. [| F : A ensures B;  A-B : insert {} CC |] ==> P A B;  
       !!A B C. [| F : A leadsTo[CC] B; P A B; F : B leadsTo[CC] C; P B C |]  
                ==> P A C;  
-      !!B S. ALL A:S. F : A leadsTo[CC] B & P A B ==> P (Union S) B  
+      !!B S. ALL A:S. F : A leadsTo[CC] B & P A B ==> P (\<Union>S) B  
    |] ==> P za zb"
 apply (unfold leadsETo_def)
 apply (drule CollectD) 
@@ -176,7 +176,7 @@
 
 lemma leadsETo_Union_Int:
  "(!!A. A : S ==> F : (A Int C) leadsTo[CC] B) 
-  ==> F : (Union S Int C) leadsTo[CC] B"
+  ==> F : (\<Union>S Int C) leadsTo[CC] B"
 apply (unfold leadsETo_def)
 apply (simp only: Int_Union_Union)
 apply (blast intro: elt.Union)
@@ -223,7 +223,7 @@
 by (blast intro: leadsETo_UN leadsETo_weaken_L)
 
 lemma leadsETo_Union_distrib:
-     "F : (Union S) leadsTo[CC] B  =  (ALL A : S. F : A leadsTo[CC] B)"
+     "F : (\<Union>S) leadsTo[CC] B  =  (ALL A : S. F : A leadsTo[CC] B)"
 by (blast intro: leadsETo_Union leadsETo_weaken_L)
 
 lemma leadsETo_weaken:
@@ -388,7 +388,7 @@
 done
 
 lemma LeadsETo_Union:
-     "(!!A. A : S ==> F : A LeadsTo[CC] B) ==> F : (Union S) LeadsTo[CC] B"
+     "(!!A. A : S ==> F : A LeadsTo[CC] B) ==> F : (\<Union>S) LeadsTo[CC] B"
 apply (simp add: LeadsETo_def)
 apply (subst Int_Union)
 apply (blast intro: leadsETo_UN)
diff -r cbd310584cff -r 546958347e05 src/HOL/UNITY/Extend.thy
--- a/src/HOL/UNITY/Extend.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/UNITY/Extend.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -255,7 +255,7 @@
 lemma extend_set_Diff_distrib: "extend_set h (A - B) = extend_set h A - extend_set h B"
   by auto
 
-lemma extend_set_Union: "extend_set h (Union A) = (\<Union>X \<in> A. extend_set h X)"
+lemma extend_set_Union: "extend_set h (\<Union>A) = (\<Union>X \<in> A. extend_set h X)"
   by blast
 
 lemma extend_set_subset_Compl_eq: "(extend_set h A \<subseteq> - extend_set h B) = (A \<subseteq> - B)"
@@ -361,7 +361,7 @@
 lemma (in -) project_set_UNIV [simp]: "project_set h UNIV = UNIV"
   by auto
 
-lemma (in -) project_set_Union: "project_set h (Union A) = (\<Union>X \<in> A. project_set h X)"
+lemma (in -) project_set_Union: "project_set h (\<Union>A) = (\<Union>X \<in> A. project_set h X)"
   by blast
 
 
@@ -561,7 +561,7 @@
 lemma slice_iff [iff]: "(x \<in> slice C y) = (h(x,y) \<in> C)"
   by (simp add: slice_def)
 
-lemma slice_Union: "slice (Union S) y = (\<Union>x \<in> S. slice x y)"
+lemma slice_Union: "slice (\<Union>S) y = (\<Union>x \<in> S. slice x y)"
   by auto
 
 lemma slice_extend_set: "slice (extend_set h A) y = A"
diff -r cbd310584cff -r 546958347e05 src/HOL/UNITY/FP.thy
--- a/src/HOL/UNITY/FP.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/UNITY/FP.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -10,7 +10,7 @@
 theory FP imports UNITY begin
 
 definition FP_Orig :: "'a program => 'a set" where
-    "FP_Orig F == Union{A. ALL B. F : stable (A Int B)}"
+    "FP_Orig F == \<Union>{A. ALL B. F : stable (A Int B)}"
 
 definition FP :: "'a program => 'a set" where
     "FP F == {s. F : stable {s}}"
diff -r cbd310584cff -r 546958347e05 src/HOL/UNITY/Guar.thy
--- a/src/HOL/UNITY/Guar.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/UNITY/Guar.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -45,11 +45,11 @@
 
   (* Weakest guarantees *)
 definition wg :: "['a program, 'a program set] => 'a program set" where
-  "wg F Y == Union({X. F \<in> X guarantees Y})"
+  "wg F Y == \<Union>({X. F \<in> X guarantees Y})"
 
    (* Weakest existential property stronger than X *)
 definition wx :: "('a program) set => ('a program)set" where
-   "wx X == Union({Y. Y \<subseteq> X & ex_prop Y})"
+   "wx X == \<Union>({Y. Y \<subseteq> X & ex_prop Y})"
   
   (*Ill-defined programs can arise through "Join"*)
 definition welldef :: "'a program set" where
diff -r cbd310584cff -r 546958347e05 src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/UNITY/SubstAx.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -61,7 +61,7 @@
 done
 
 lemma LeadsTo_Union: 
-     "(!!A. A \<in> S ==> F \<in> A LeadsTo B) ==> F \<in> (Union S) LeadsTo B"
+     "(!!A. A \<in> S ==> F \<in> A LeadsTo B) ==> F \<in> (\<Union>S) LeadsTo B"
 apply (simp add: LeadsTo_def)
 apply (subst Int_Union)
 apply (blast intro: leadsTo_UN)
@@ -152,7 +152,7 @@
 by (blast intro: LeadsTo_UN LeadsTo_weaken_L)
 
 lemma LeadsTo_Union_distrib:
-     "(F \<in> (Union S) LeadsTo B)  =  (\<forall>A \<in> S. F \<in> A LeadsTo B)"
+     "(F \<in> (\<Union>S) LeadsTo B)  =  (\<forall>A \<in> S. F \<in> A LeadsTo B)"
 by (blast intro: LeadsTo_Union LeadsTo_weaken_L)
 
 
diff -r cbd310584cff -r 546958347e05 src/HOL/UNITY/UNITY.thy
--- a/src/HOL/UNITY/UNITY.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/UNITY/UNITY.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -48,7 +48,7 @@
     "stable A == A co A"
 
 definition strongest_rhs :: "['a program, 'a set] => 'a set" where
-    "strongest_rhs F A == Inter {B. F \<in> A co B}"
+    "strongest_rhs F A == \<Inter>{B. F \<in> A co B}"
 
 definition invariant :: "'a set => 'a program set" where
     "invariant A == {F. Init F \<subseteq> A} \<inter> stable A"
@@ -343,7 +343,7 @@
 lemma Un_Diff_Diff [simp]: "A \<union> B - (A - B) = B"
 by blast
 
-lemma Int_Union_Union: "Union(B) \<inter> A = Union((%C. C \<inter> A)`B)"
+lemma Int_Union_Union: "\<Union>B \<inter> A = \<Union>((%C. C \<inter> A)`B)"
 by blast
 
 text{*Needed for WF reasoning in WFair.thy*}
diff -r cbd310584cff -r 546958347e05 src/HOL/UNITY/WFair.thy
--- a/src/HOL/UNITY/WFair.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/UNITY/WFair.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -65,7 +65,7 @@
   
 definition wlt :: "['a program, 'a set] => 'a set" where
      --{*predicate transformer: the largest set that leads to @{term B}*}
-    "wlt F B == Union {A. F \<in> A leadsTo B}"
+    "wlt F B == \<Union>{A. F \<in> A leadsTo B}"
 
 notation leadsTo  (infixl "\<longmapsto>" 60)
 
@@ -189,13 +189,13 @@
 
 text{*The Union introduction rule as we should have liked to state it*}
 lemma leadsTo_Union: 
-    "(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (Union S) leadsTo B"
+    "(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (\<Union>S) leadsTo B"
 apply (unfold leadsTo_def)
 apply (blast intro: leads.Union)
 done
 
 lemma leadsTo_Union_Int: 
- "(!!A. A \<in> S ==> F \<in> (A \<inter> C) leadsTo B) ==> F \<in> (Union S \<inter> C) leadsTo B"
+ "(!!A. A \<in> S ==> F \<in> (A \<inter> C) leadsTo B) ==> F \<in> (\<Union>S \<inter> C) leadsTo B"
 apply (unfold leadsTo_def)
 apply (simp only: Int_Union_Union)
 apply (blast intro: leads.Union)
@@ -223,7 +223,7 @@
       !!A B. F \<in> A ensures B ==> P A B;  
       !!A B C. [| F \<in> A leadsTo B; P A B; F \<in> B leadsTo C; P B C |]  
                ==> P A C;  
-      !!B S. \<forall>A \<in> S. F \<in> A leadsTo B & P A B ==> P (Union S) B  
+      !!B S. \<forall>A \<in> S. F \<in> A leadsTo B & P A B ==> P (\<Union>S) B  
    |] ==> P za zb"
 apply (unfold leadsTo_def)
 apply (drule CollectD, erule leads.induct)
@@ -251,7 +251,7 @@
   "[| F \<in> za leadsTo zb;   
       P zb;  
       !!A B. [| F \<in> A ensures B;  P B |] ==> P A;  
-      !!S. \<forall>A \<in> S. P A ==> P (Union S)  
+      !!S. \<forall>A \<in> S. P A ==> P (\<Union>S)  
    |] ==> P za"
 txt{*by induction on this formula*}
 apply (subgoal_tac "P zb --> P za")
@@ -265,7 +265,7 @@
   "[| F \<in> za leadsTo zb;   
       P zb;  
       !!A B. [| F \<in> A ensures B;  F \<in> B leadsTo zb;  P B |] ==> P A;  
-      !!S. \<forall>A \<in> S. F \<in> A leadsTo zb & P A ==> P (Union S)  
+      !!S. \<forall>A \<in> S. F \<in> A leadsTo zb & P A ==> P (\<Union>S)  
    |] ==> P za"
 apply (subgoal_tac "F \<in> za leadsTo zb & P za")
 apply (erule conjunct2)
@@ -293,7 +293,7 @@
 by (blast intro: leadsTo_UN leadsTo_weaken_L)
 
 lemma leadsTo_Union_distrib:
-     "F \<in> (Union S) leadsTo B  =  (\<forall>A \<in> S. F \<in> A leadsTo B)"
+     "F \<in> (\<Union>S) leadsTo B  =  (\<forall>A \<in> S. F \<in> A leadsTo B)"
 by (blast intro: leadsTo_Union leadsTo_weaken_L)
 
 
diff -r cbd310584cff -r 546958347e05 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -305,7 +305,7 @@
 lemma wf_Union: 
  "[| ALL r:R. wf r;  
      ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}  
-  |] ==> wf(Union R)"
+  |] ==> wf (\<Union> R)"
   using wf_UN[of R "\<lambda>i. i"] by simp
 
 (*Intuition: we find an (R u S)-min element of a nonempty subset A