prefer symbols for "Union", "Inter";
authorwenzelm
Mon Dec 28 17:43:30 2015 +0100 (2015-12-28)
changeset 61952546958347e05
parent 61951 cbd310584cff
child 61953 7247cb62406c
prefer symbols for "Union", "Inter";
src/HOL/Algebra/Ideal.thy
src/HOL/Cardinals/Cardinal_Order_Relation.thy
src/HOL/Cardinals/Wellorder_Relation.thy
src/HOL/Complete_Lattices.thy
src/HOL/Equiv_Relations.thy
src/HOL/Groups_Big.thy
src/HOL/Inductive.thy
src/HOL/Library/Countable_Set_Type.thy
src/HOL/Library/FSet.thy
src/HOL/Library/Old_Datatype.thy
src/HOL/Lifting_Set.thy
src/HOL/MicroJava/BV/BVExample.thy
src/HOL/MicroJava/BV/JVMType.thy
src/HOL/MicroJava/DFA/Err.thy
src/HOL/MicroJava/DFA/Listn.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Number_Theory/MiscAlgebra.thy
src/HOL/Old_Number_Theory/Euler.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
src/HOL/UNITY/ELT.thy
src/HOL/UNITY/Extend.thy
src/HOL/UNITY/FP.thy
src/HOL/UNITY/Guar.thy
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/UNITY.thy
src/HOL/UNITY/WFair.thy
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Algebra/Ideal.thy	Mon Dec 28 16:34:26 2015 +0100
     1.2 +++ b/src/HOL/Algebra/Ideal.thy	Mon Dec 28 17:43:30 2015 +0100
     1.3 @@ -47,7 +47,7 @@
     1.4  subsubsection (in ring) \<open>Ideals Generated by a Subset of @{term "carrier R"}\<close>
     1.5  
     1.6  definition genideal :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set"  ("Idl\<index> _" [80] 79)
     1.7 -  where "genideal R S = Inter {I. ideal I R \<and> S \<subseteq> I}"
     1.8 +  where "genideal R S = \<Inter>{I. ideal I R \<and> S \<subseteq> I}"
     1.9  
    1.10  subsubsection \<open>Principal Ideals\<close>
    1.11  
    1.12 @@ -218,7 +218,7 @@
    1.13  lemma (in ring) i_Intersect:
    1.14    assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R"
    1.15      and notempty: "S \<noteq> {}"
    1.16 -  shows "ideal (Inter S) R"
    1.17 +  shows "ideal (\<Inter>S) R"
    1.18    apply (unfold_locales)
    1.19    apply (simp_all add: Inter_eq)
    1.20          apply rule unfolding mem_Collect_eq defer 1
     2.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Mon Dec 28 16:34:26 2015 +0100
     2.2 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Mon Dec 28 17:43:30 2015 +0100
     2.3 @@ -785,9 +785,9 @@
     2.4  lemma Card_order_lists: "Card_order r \<Longrightarrow> r \<le>o |lists(Field r) |"
     2.5  using card_of_lists card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
     2.6  
     2.7 -lemma Union_set_lists:
     2.8 -"Union(set ` (lists A)) = A"
     2.9 -unfolding lists_def2 proof(auto)
    2.10 +lemma Union_set_lists: "\<Union>(set ` (lists A)) = A"
    2.11 +  unfolding lists_def2
    2.12 +proof(auto)
    2.13    fix a assume "a \<in> A"
    2.14    hence "set [a] \<le> A \<and> a \<in> set [a]" by auto
    2.15    thus "\<exists>l. set l \<le> A \<and> a \<in> set l" by blast
     3.1 --- a/src/HOL/Cardinals/Wellorder_Relation.thy	Mon Dec 28 16:34:26 2015 +0100
     3.2 +++ b/src/HOL/Cardinals/Wellorder_Relation.thy	Mon Dec 28 17:43:30 2015 +0100
     3.3 @@ -441,15 +441,15 @@
     3.4  unfolding ofilter_def by blast
     3.5  
     3.6  lemma ofilter_Inter:
     3.7 -"\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> ofilter A\<rbrakk> \<Longrightarrow> ofilter (Inter S)"
     3.8 +"\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> ofilter A\<rbrakk> \<Longrightarrow> ofilter (\<Inter>S)"
     3.9  unfolding ofilter_def by blast
    3.10  
    3.11  lemma ofilter_Union:
    3.12 -"(\<And> A. A \<in> S \<Longrightarrow> ofilter A) \<Longrightarrow> ofilter (Union S)"
    3.13 +"(\<And> A. A \<in> S \<Longrightarrow> ofilter A) \<Longrightarrow> ofilter (\<Union>S)"
    3.14  unfolding ofilter_def by blast
    3.15  
    3.16  lemma ofilter_under_Union:
    3.17 -"ofilter A \<Longrightarrow> A = Union {under a| a. a \<in> A}"
    3.18 +"ofilter A \<Longrightarrow> A = \<Union>{under a| a. a \<in> A}"
    3.19  using ofilter_under_UNION[of A]
    3.20  by(unfold Union_eq, auto)
    3.21  
     4.1 --- a/src/HOL/Complete_Lattices.thy	Mon Dec 28 16:34:26 2015 +0100
     4.2 +++ b/src/HOL/Complete_Lattices.thy	Mon Dec 28 17:43:30 2015 +0100
     4.3 @@ -901,12 +901,9 @@
     4.4  
     4.5  subsubsection \<open>Inter\<close>
     4.6  
     4.7 -abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
     4.8 -  "Inter S \<equiv> \<Sqinter>S"
     4.9 +abbreviation Inter :: "'a set set \<Rightarrow> 'a set"  ("\<Inter>_" [900] 900)
    4.10 +  where "\<Inter>S \<equiv> \<Sqinter>S"
    4.11    
    4.12 -notation (xsymbols)
    4.13 -  Inter  ("\<Inter>_" [900] 900)
    4.14 -
    4.15  lemma Inter_eq:
    4.16    "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
    4.17  proof (rule set_eqI)
    4.18 @@ -944,7 +941,7 @@
    4.19    "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B"
    4.20    by (fact Inf_less_eq)
    4.21  
    4.22 -lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> Inter A"
    4.23 +lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> \<Inter>A"
    4.24    by (fact Inf_greatest)
    4.25  
    4.26  lemma Inter_empty: "\<Inter>{} = UNIV"
    4.27 @@ -1080,11 +1077,8 @@
    4.28  
    4.29  subsubsection \<open>Union\<close>
    4.30  
    4.31 -abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
    4.32 -  "Union S \<equiv> \<Squnion>S"
    4.33 -
    4.34 -notation (xsymbols)
    4.35 -  Union  ("\<Union>_" [900] 900)
    4.36 +abbreviation Union :: "'a set set \<Rightarrow> 'a set"  ("\<Union>_" [900] 900)
    4.37 +  where "\<Union>S \<equiv> \<Squnion>S"
    4.38  
    4.39  lemma Union_eq:
    4.40    "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
     5.1 --- a/src/HOL/Equiv_Relations.thy	Mon Dec 28 16:34:26 2015 +0100
     5.2 +++ b/src/HOL/Equiv_Relations.thy	Mon Dec 28 17:43:30 2015 +0100
     5.3 @@ -108,7 +108,7 @@
     5.4    "X \<in> A//r ==> (!!x. X = r``{x} ==> x \<in> A ==> P) ==> P"
     5.5    by (unfold quotient_def) blast
     5.6  
     5.7 -lemma Union_quotient: "equiv A r ==> Union (A//r) = A"
     5.8 +lemma Union_quotient: "equiv A r ==> \<Union>(A//r) = A"
     5.9    by (unfold equiv_def refl_on_def quotient_def) blast
    5.10  
    5.11  lemma quotient_disj:
     6.1 --- a/src/HOL/Groups_Big.thy	Mon Dec 28 16:34:26 2015 +0100
     6.2 +++ b/src/HOL/Groups_Big.thy	Mon Dec 28 17:43:30 2015 +0100
     6.3 @@ -172,7 +172,7 @@
     6.4  
     6.5  lemma Union_disjoint:
     6.6    assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
     6.7 -  shows "F g (Union C) = (F \<circ> F) g C"
     6.8 +  shows "F g (\<Union>C) = (F \<circ> F) g C"
     6.9  proof cases
    6.10    assume "finite C"
    6.11    from UNION_disjoint [OF this assms]
    6.12 @@ -994,7 +994,7 @@
    6.13  lemma card_Union_disjoint:
    6.14    "finite C ==> (ALL A:C. finite A) ==>
    6.15     (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
    6.16 -   ==> card (Union C) = setsum card C"
    6.17 +   ==> card (\<Union>C) = setsum card C"
    6.18  apply (frule card_UN_disjoint [of C id])
    6.19  apply simp_all
    6.20  done
     7.1 --- a/src/HOL/Inductive.thy	Mon Dec 28 16:34:26 2015 +0100
     7.2 +++ b/src/HOL/Inductive.thy	Mon Dec 28 17:43:30 2015 +0100
     7.3 @@ -87,16 +87,16 @@
     7.4  
     7.5  lemma lfp_induct_set:
     7.6    assumes lfp: "a: lfp(f)"
     7.7 -      and mono: "mono(f)"
     7.8 -      and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
     7.9 +    and mono: "mono(f)"
    7.10 +    and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
    7.11    shows "P(a)"
    7.12    by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
    7.13       (auto simp: intro: indhyp)
    7.14  
    7.15  lemma lfp_ordinal_induct_set: 
    7.16    assumes mono: "mono f"
    7.17 -  and P_f: "!!S. P S ==> P(f S)"
    7.18 -  and P_Union: "!!M. !S:M. P S ==> P(Union M)"
    7.19 +    and P_f: "!!S. P S ==> P(f S)"
    7.20 +    and P_Union: "!!M. !S:M. P S ==> P (\<Union>M)"
    7.21    shows "P(lfp f)"
    7.22    using assms by (rule lfp_ordinal_induct)
    7.23  
     8.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Mon Dec 28 16:34:26 2015 +0100
     8.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Mon Dec 28 17:43:30 2015 +0100
     8.3 @@ -118,7 +118,7 @@
     8.4    is "UNION" parametric UNION_transfer by simp
     8.5  definition cUnion :: "'a cset cset \<Rightarrow> 'a cset" where "cUnion A = cUNION A id"
     8.6  
     8.7 -lemma Union_conv_UNION: "Union A = UNION A id"
     8.8 +lemma Union_conv_UNION: "\<Union>A = UNION A id"
     8.9  by auto
    8.10  
    8.11  lemma cUnion_transfer [transfer_rule]:
     9.1 --- a/src/HOL/Library/FSet.thy	Mon Dec 28 16:34:26 2015 +0100
     9.2 +++ b/src/HOL/Library/FSet.thy	Mon Dec 28 17:43:30 2015 +0100
     9.3 @@ -79,7 +79,7 @@
     9.4  lemma right_total_Inf_fset_transfer:
     9.5    assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
     9.6    shows "(rel_set (rel_set A) ===> rel_set A) 
     9.7 -    (\<lambda>S. if finite (Inter S \<inter> Collect (Domainp A)) then Inter S \<inter> Collect (Domainp A) else {}) 
     9.8 +    (\<lambda>S. if finite (\<Inter>S \<inter> Collect (Domainp A)) then \<Inter>S \<inter> Collect (Domainp A) else {}) 
     9.9        (\<lambda>S. if finite (Inf S) then Inf S else {})"
    9.10      by transfer_prover
    9.11  
    10.1 --- a/src/HOL/Library/Old_Datatype.thy	Mon Dec 28 16:34:26 2015 +0100
    10.2 +++ b/src/HOL/Library/Old_Datatype.thy	Mon Dec 28 17:43:30 2015 +0100
    10.3 @@ -76,7 +76,7 @@
    10.4    In1_def:    "In1(M) == Scons (Numb 1) M"
    10.5  
    10.6    (*Function spaces*)
    10.7 -  Lim_def: "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}"
    10.8 +  Lim_def: "Lim f == \<Union>{z. ? x. z = Push_Node (Inl x) ` (f x)}"
    10.9  
   10.10    (*the set of nodes with depth less than k*)
   10.11    ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
    11.1 --- a/src/HOL/Lifting_Set.thy	Mon Dec 28 16:34:26 2015 +0100
    11.2 +++ b/src/HOL/Lifting_Set.thy	Mon Dec 28 17:43:30 2015 +0100
    11.3 @@ -237,7 +237,7 @@
    11.4  
    11.5  lemma right_total_Inter_transfer [transfer_rule]:
    11.6    assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
    11.7 -  shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>S. Inter S \<inter> Collect (Domainp A)) Inter"
    11.8 +  shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>S. \<Inter>S \<inter> Collect (Domainp A)) Inter"
    11.9    unfolding Inter_eq[abs_def]
   11.10    by (subst Collect_conj_eq[symmetric]) transfer_prover
   11.11  
    12.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Mon Dec 28 16:34:26 2015 +0100
    12.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon Dec 28 17:43:30 2015 +0100
    12.3 @@ -424,7 +424,7 @@
    12.4      apply (case_tac "\<not> stable r step ss p")
    12.5      apply simp_all
    12.6      done
    12.7 -  also have "\<And>f. (UN p:{..<size ss}. f p) = Union (set (map f [0..<size ss]))" by auto
    12.8 +  also have "\<And>f. (UN p:{..<size ss}. f p) = \<Union>(set (map f [0..<size ss]))" by auto
    12.9    also note Sup_set_fold also note fold_map
   12.10    also have "op \<union> \<circ> (\<lambda>p. if \<not> stable r step ss p then {p} else {}) = 
   12.11              (\<lambda>p A. if \<not>stable r step ss p then insert p A else A)"
    13.1 --- a/src/HOL/MicroJava/BV/JVMType.thy	Mon Dec 28 16:34:26 2015 +0100
    13.2 +++ b/src/HOL/MicroJava/BV/JVMType.thy	Mon Dec 28 17:43:30 2015 +0100
    13.3 @@ -62,7 +62,7 @@
    13.4                     
    13.5  
    13.6  lemma JVM_states_unfold: 
    13.7 -  "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) \<times>
    13.8 +  "states S maxs maxr == err(opt((\<Union>{list n (types S) |n. n <= maxs}) \<times>
    13.9                                    list maxr (err(types S))))"
   13.10    apply (unfold states_def sl_def Opt.esl_def Err.sl_def
   13.11           stk_esl_def reg_sl_def Product.esl_def
    14.1 --- a/src/HOL/MicroJava/DFA/Err.thy	Mon Dec 28 16:34:26 2015 +0100
    14.2 +++ b/src/HOL/MicroJava/DFA/Err.thy	Mon Dec 28 17:43:30 2015 +0100
    14.3 @@ -283,7 +283,7 @@
    14.4    done 
    14.5  qed
    14.6  
    14.7 -subsection \<open>semilat (err(Union AS))\<close>
    14.8 +subsection \<open>semilat (err (Union AS))\<close>
    14.9  
   14.10  (* FIXME? *)
   14.11  lemma all_bex_swap_lemma [iff]:
   14.12 @@ -293,7 +293,7 @@
   14.13  lemma closed_err_Union_lift2I: 
   14.14    "\<lbrakk> !A:AS. closed (err A) (lift2 f); AS ~= {}; 
   14.15        !A:AS.!B:AS. A~=B \<longrightarrow> (!a:A.!b:B. a +_f b = Err) \<rbrakk> 
   14.16 -  \<Longrightarrow> closed (err(Union AS)) (lift2 f)"
   14.17 +  \<Longrightarrow> closed (err (\<Union>AS)) (lift2 f)"
   14.18  apply (unfold closed_def err_def)
   14.19  apply simp
   14.20  apply clarify
   14.21 @@ -309,7 +309,7 @@
   14.22  lemma err_semilat_UnionI:
   14.23    "\<lbrakk> !A:AS. err_semilat(A, r, f); AS ~= {}; 
   14.24        !A:AS.!B:AS. A~=B \<longrightarrow> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) \<rbrakk> 
   14.25 -  \<Longrightarrow> err_semilat(Union AS, r, f)"
   14.26 +  \<Longrightarrow> err_semilat (\<Union>AS, r, f)"
   14.27  apply (unfold semilat_def sl_def)
   14.28  apply (simp add: closed_err_Union_lift2I)
   14.29  apply (rule conjI)
    15.1 --- a/src/HOL/MicroJava/DFA/Listn.thy	Mon Dec 28 16:34:26 2015 +0100
    15.2 +++ b/src/HOL/MicroJava/DFA/Listn.thy	Mon Dec 28 17:43:30 2015 +0100
    15.3 @@ -44,7 +44,7 @@
    15.4  "sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err"
    15.5  
    15.6  definition upto_esl :: "nat \<Rightarrow> 'a esl \<Rightarrow> 'a list esl" where
    15.7 -"upto_esl m == %(A,r,f). (Union{list n A |n. n <= m}, le r, sup f)"
    15.8 +"upto_esl m == %(A,r,f). (\<Union>{list n A |n. n <= m}, le r, sup f)"
    15.9  
   15.10  lemmas [simp] = set_update_subsetI
   15.11  
    16.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Dec 28 16:34:26 2015 +0100
    16.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Dec 28 17:43:30 2015 +0100
    16.3 @@ -74,7 +74,7 @@
    16.4    finally show ?thesis .
    16.5  qed
    16.6  
    16.7 -lemma subspace_Inter: "\<forall>s \<in> f. subspace s \<Longrightarrow> subspace (Inter f)"
    16.8 +lemma subspace_Inter: "\<forall>s \<in> f. subspace s \<Longrightarrow> subspace (\<Inter>f)"
    16.9    unfolding subspace_def by auto
   16.10  
   16.11  lemma span_eq[simp]: "span s = s \<longleftrightarrow> subspace s"
   16.12 @@ -1110,7 +1110,7 @@
   16.13  lemma cone_0: "cone {0}"
   16.14    unfolding cone_def by auto
   16.15  
   16.16 -lemma cone_Union[intro]: "(\<forall>s\<in>f. cone s) \<longrightarrow> cone (Union f)"
   16.17 +lemma cone_Union[intro]: "(\<forall>s\<in>f. cone s) \<longrightarrow> cone (\<Union>f)"
   16.18    unfolding cone_def by blast
   16.19  
   16.20  lemma cone_iff:
   16.21 @@ -8075,7 +8075,7 @@
   16.22        assume z: "z \<in> \<Inter>{rel_interior S |S. S \<in> I}"
   16.23        {
   16.24          fix x
   16.25 -        assume x: "x \<in> Inter I"
   16.26 +        assume x: "x \<in> \<Inter>I"
   16.27          {
   16.28            fix S
   16.29            assume S: "S \<in> I"
    17.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 28 16:34:26 2015 +0100
    17.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 28 17:43:30 2015 +0100
    17.3 @@ -203,13 +203,13 @@
    17.4  
    17.5  lemma open_countable_basis_ex:
    17.6    assumes "open X"
    17.7 -  shows "\<exists>B' \<subseteq> B. X = Union B'"
    17.8 +  shows "\<exists>B' \<subseteq> B. X = \<Union>B'"
    17.9    using assms countable_basis is_basis
   17.10    unfolding topological_basis_def by blast
   17.11  
   17.12  lemma open_countable_basisE:
   17.13    assumes "open X"
   17.14 -  obtains B' where "B' \<subseteq> B" "X = Union B'"
   17.15 +  obtains B' where "B' \<subseteq> B" "X = \<Union>B'"
   17.16    using assms open_countable_basis_ex
   17.17    by (atomize_elim) simp
   17.18  
   17.19 @@ -1885,7 +1885,7 @@
   17.20  lemma connected_component_of_subset: "\<lbrakk>connected_component s x y; s \<subseteq> t\<rbrakk> \<Longrightarrow> connected_component t x y"
   17.21    by (auto simp: connected_component_def)
   17.22  
   17.23 -lemma connected_component_Union: "connected_component_set s x = Union {t. connected t \<and> x \<in> t \<and> t \<subseteq> s}"
   17.24 +lemma connected_component_Union: "connected_component_set s x = \<Union>{t. connected t \<and> x \<in> t \<and> t \<subseteq> s}"
   17.25    by (auto simp: connected_component_def)
   17.26  
   17.27  lemma connected_connected_component [iff]: "connected (connected_component_set s x)"
   17.28 @@ -2024,7 +2024,7 @@
   17.29  by (metis (no_types, hide_lams) connected_component_eq_eq connected_component_in connected_component_maximal subsetD mem_Collect_eq)
   17.30  
   17.31  
   17.32 -lemma Union_connected_component: "Union (connected_component_set s ` s) = s"
   17.33 +lemma Union_connected_component: "\<Union>(connected_component_set s ` s) = s"
   17.34    apply (rule subset_antisym)
   17.35    apply (simp add: SUP_least connected_component_subset)
   17.36    using connected_component_refl_eq
   17.37 @@ -2033,7 +2033,7 @@
   17.38  
   17.39  lemma complement_connected_component_unions:
   17.40      "s - connected_component_set s x =
   17.41 -     Union (connected_component_set s ` s - {connected_component_set s x})"
   17.42 +     \<Union>(connected_component_set s ` s - {connected_component_set s x})"
   17.43    apply (subst Union_connected_component [symmetric], auto)
   17.44    apply (metis connected_component_eq_eq connected_component_in)
   17.45    by (metis connected_component_eq mem_Collect_eq)
   17.46 @@ -2053,7 +2053,7 @@
   17.47  lemma components_iff: "s \<in> components u \<longleftrightarrow> (\<exists>x. x \<in> u \<and> s = connected_component_set u x)"
   17.48    by (auto simp: components_def)
   17.49  
   17.50 -lemma Union_components: "u = Union (components u)"
   17.51 +lemma Union_components: "u = \<Union>(components u)"
   17.52    apply (rule subset_antisym)
   17.53    apply (metis Union_connected_component components_def set_eq_subset)
   17.54    using Union_connected_component components_def by fastforce
   17.55 @@ -2142,7 +2142,7 @@
   17.56    apply (auto simp: components_iff)
   17.57    by (metis connected_component_eq_empty connected_component_intermediate_subset)
   17.58  
   17.59 -lemma in_components_unions_complement: "c \<in> components s \<Longrightarrow> s - c = Union(components s - {c})"
   17.60 +lemma in_components_unions_complement: "c \<in> components s \<Longrightarrow> s - c = \<Union>(components s - {c})"
   17.61    by (metis complement_connected_component_unions components_def components_iff)
   17.62  
   17.63  lemma connected_intermediate_closure:
    18.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy	Mon Dec 28 16:34:26 2015 +0100
    18.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Mon Dec 28 17:43:30 2015 +0100
    18.3 @@ -257,7 +257,7 @@
    18.4  lemma (in comm_monoid) finprod_Union_disjoint:
    18.5    "[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G));
    18.6        (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
    18.7 -   ==> finprod G f (Union C) = finprod G (finprod G f) C"
    18.8 +   ==> finprod G f (\<Union>C) = finprod G (finprod G f) C"
    18.9    apply (frule finprod_UN_disjoint [of C id f])
   18.10    apply (auto simp add: SUP_def)
   18.11    done
    19.1 --- a/src/HOL/Old_Number_Theory/Euler.thy	Mon Dec 28 16:34:26 2015 +0100
    19.2 +++ b/src/HOL/Old_Number_Theory/Euler.thy	Mon Dec 28 17:43:30 2015 +0100
    19.3 @@ -49,7 +49,7 @@
    19.4    by (auto simp add: MultInvPair_prop1b)
    19.5  
    19.6  lemma MultInvPair_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> 
    19.7 -                          Union ( SetS a p) = SRStar p"
    19.8 +                          \<Union>(SetS a p) = SRStar p"
    19.9    apply (auto simp add: SetS_def MultInvPair_def StandardRes_SRStar_prop4 
   19.10      SRStar_mult_prop2)
   19.11    apply (frule StandardRes_SRStar_prop3)
   19.12 @@ -105,7 +105,7 @@
   19.13    apply (rule MultInvPair_card_two, auto)
   19.14    done
   19.15  
   19.16 -lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))"
   19.17 +lemma Union_SetS_finite: "2 < p ==> finite (\<Union>(SetS a p))"
   19.18    by (auto simp add: SetS_finite SetS_elems_finite)
   19.19  
   19.20  lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set); 
   19.21 @@ -118,7 +118,7 @@
   19.22  proof -
   19.23    have "(p - 1) = 2 * int(card(SetS a p))"
   19.24    proof -
   19.25 -    have "p - 1 = int(card(Union (SetS a p)))"
   19.26 +    have "p - 1 = int(card(\<Union>(SetS a p)))"
   19.27        by (auto simp add: assms MultInvPair_prop2 SRStar_card)
   19.28      also have "... = int (setsum card (SetS a p))"
   19.29        by (auto simp add: assms SetS_finite SetS_elems_finite
   19.30 @@ -177,9 +177,9 @@
   19.31  lemma Union_SetS_setprod_prop1:
   19.32    assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and
   19.33      "~(QuadRes p a)"
   19.34 -  shows "[\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
   19.35 +  shows "[\<Prod>(\<Union>(SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
   19.36  proof -
   19.37 -  from assms have "[\<Prod>(Union (SetS a p)) = setprod (setprod (%x. x)) (SetS a p)] (mod p)"
   19.38 +  from assms have "[\<Prod>(\<Union>(SetS a p)) = setprod (setprod (%x. x)) (SetS a p)] (mod p)"
   19.39      by (auto simp add: SetS_finite SetS_elems_finite
   19.40        MultInvPair_prop1c setprod.Union_disjoint)
   19.41    also have "[setprod (setprod (%x. x)) (SetS a p) = 
   19.42 @@ -199,9 +199,9 @@
   19.43  
   19.44  lemma Union_SetS_setprod_prop2:
   19.45    assumes "zprime p" and "2 < p" and "~([a = 0](mod p))"
   19.46 -  shows "\<Prod>(Union (SetS a p)) = zfact (p - 1)"
   19.47 +  shows "\<Prod>(\<Union>(SetS a p)) = zfact (p - 1)"
   19.48  proof -
   19.49 -  from assms have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)"
   19.50 +  from assms have "\<Prod>(\<Union>(SetS a p)) = \<Prod>(SRStar p)"
   19.51      by (auto simp add: MultInvPair_prop2)
   19.52    also have "... = \<Prod>({1} \<union> (d22set (p - 1)))"
   19.53      by (auto simp add: assms SRStar_d22set_prop)
    20.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Mon Dec 28 16:34:26 2015 +0100
    20.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Mon Dec 28 17:43:30 2015 +0100
    20.3 @@ -75,7 +75,7 @@
    20.4    assumes Un [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M"
    20.5  
    20.6  lemma (in ring_of_sets) finite_Union [intro]:
    20.7 -  "finite X \<Longrightarrow> X \<subseteq> M \<Longrightarrow> Union X \<in> M"
    20.8 +  "finite X \<Longrightarrow> X \<subseteq> M \<Longrightarrow> \<Union>X \<in> M"
    20.9    by (induct set: finite) (auto simp add: Un)
   20.10  
   20.11  lemma (in ring_of_sets) finite_UN[intro]:
   20.12 @@ -261,7 +261,7 @@
   20.13  qed
   20.14  
   20.15  lemma (in sigma_algebra) countable_Union [intro]:
   20.16 -  assumes "countable X" "X \<subseteq> M" shows "Union X \<in> M"
   20.17 +  assumes "countable X" "X \<subseteq> M" shows "\<Union>X \<in> M"
   20.18  proof cases
   20.19    assume "X \<noteq> {}"
   20.20    hence "\<Union>X = (\<Union>n. from_nat_into X n)"
    21.1 --- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Mon Dec 28 16:34:26 2015 +0100
    21.2 +++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Mon Dec 28 17:43:30 2015 +0100
    21.3 @@ -105,7 +105,7 @@
    21.4  
    21.5  primrec used :: "event list => msg set"
    21.6  where
    21.7 -  used_Nil:   "used []         = Union (parts ` initState ` agents)"
    21.8 +  used_Nil:   "used []         = \<Union>(parts ` initState ` agents)"
    21.9  | used_Cons:  "used (ev # evs) =
   21.10                       (case ev of
   21.11                          Says A B X => parts {X} \<union> used evs
   21.12 @@ -172,13 +172,13 @@
   21.13  
   21.14  lemma [code]:
   21.15    "analz H = (let
   21.16 -     H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
   21.17 +     H' = H \<union> (\<Union>((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
   21.18     in if H' = H then H else analz H')"
   21.19  sorry
   21.20  
   21.21  lemma [code]:
   21.22    "parts H = (let
   21.23 -     H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
   21.24 +     H' = H \<union> (\<Union>((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
   21.25     in if H' = H then H else parts H')"
   21.26  sorry
   21.27  
    22.1 --- a/src/HOL/UNITY/ELT.thy	Mon Dec 28 16:34:26 2015 +0100
    22.2 +++ b/src/HOL/UNITY/ELT.thy	Mon Dec 28 17:43:30 2015 +0100
    22.3 @@ -133,7 +133,7 @@
    22.4  
    22.5  (*The Union introduction rule as we should have liked to state it*)
    22.6  lemma leadsETo_Union:
    22.7 -    "(!!A. A : S ==> F : A leadsTo[CC] B) ==> F : (Union S) leadsTo[CC] B"
    22.8 +    "(!!A. A : S ==> F : A leadsTo[CC] B) ==> F : (\<Union>S) leadsTo[CC] B"
    22.9  apply (unfold leadsETo_def)
   22.10  apply (blast intro: elt.Union)
   22.11  done
   22.12 @@ -151,7 +151,7 @@
   22.13        !!A B. [| F : A ensures B;  A-B : insert {} CC |] ==> P A B;  
   22.14        !!A B C. [| F : A leadsTo[CC] B; P A B; F : B leadsTo[CC] C; P B C |]  
   22.15                 ==> P A C;  
   22.16 -      !!B S. ALL A:S. F : A leadsTo[CC] B & P A B ==> P (Union S) B  
   22.17 +      !!B S. ALL A:S. F : A leadsTo[CC] B & P A B ==> P (\<Union>S) B  
   22.18     |] ==> P za zb"
   22.19  apply (unfold leadsETo_def)
   22.20  apply (drule CollectD) 
   22.21 @@ -176,7 +176,7 @@
   22.22  
   22.23  lemma leadsETo_Union_Int:
   22.24   "(!!A. A : S ==> F : (A Int C) leadsTo[CC] B) 
   22.25 -  ==> F : (Union S Int C) leadsTo[CC] B"
   22.26 +  ==> F : (\<Union>S Int C) leadsTo[CC] B"
   22.27  apply (unfold leadsETo_def)
   22.28  apply (simp only: Int_Union_Union)
   22.29  apply (blast intro: elt.Union)
   22.30 @@ -223,7 +223,7 @@
   22.31  by (blast intro: leadsETo_UN leadsETo_weaken_L)
   22.32  
   22.33  lemma leadsETo_Union_distrib:
   22.34 -     "F : (Union S) leadsTo[CC] B  =  (ALL A : S. F : A leadsTo[CC] B)"
   22.35 +     "F : (\<Union>S) leadsTo[CC] B  =  (ALL A : S. F : A leadsTo[CC] B)"
   22.36  by (blast intro: leadsETo_Union leadsETo_weaken_L)
   22.37  
   22.38  lemma leadsETo_weaken:
   22.39 @@ -388,7 +388,7 @@
   22.40  done
   22.41  
   22.42  lemma LeadsETo_Union:
   22.43 -     "(!!A. A : S ==> F : A LeadsTo[CC] B) ==> F : (Union S) LeadsTo[CC] B"
   22.44 +     "(!!A. A : S ==> F : A LeadsTo[CC] B) ==> F : (\<Union>S) LeadsTo[CC] B"
   22.45  apply (simp add: LeadsETo_def)
   22.46  apply (subst Int_Union)
   22.47  apply (blast intro: leadsETo_UN)
    23.1 --- a/src/HOL/UNITY/Extend.thy	Mon Dec 28 16:34:26 2015 +0100
    23.2 +++ b/src/HOL/UNITY/Extend.thy	Mon Dec 28 17:43:30 2015 +0100
    23.3 @@ -255,7 +255,7 @@
    23.4  lemma extend_set_Diff_distrib: "extend_set h (A - B) = extend_set h A - extend_set h B"
    23.5    by auto
    23.6  
    23.7 -lemma extend_set_Union: "extend_set h (Union A) = (\<Union>X \<in> A. extend_set h X)"
    23.8 +lemma extend_set_Union: "extend_set h (\<Union>A) = (\<Union>X \<in> A. extend_set h X)"
    23.9    by blast
   23.10  
   23.11  lemma extend_set_subset_Compl_eq: "(extend_set h A \<subseteq> - extend_set h B) = (A \<subseteq> - B)"
   23.12 @@ -361,7 +361,7 @@
   23.13  lemma (in -) project_set_UNIV [simp]: "project_set h UNIV = UNIV"
   23.14    by auto
   23.15  
   23.16 -lemma (in -) project_set_Union: "project_set h (Union A) = (\<Union>X \<in> A. project_set h X)"
   23.17 +lemma (in -) project_set_Union: "project_set h (\<Union>A) = (\<Union>X \<in> A. project_set h X)"
   23.18    by blast
   23.19  
   23.20  
   23.21 @@ -561,7 +561,7 @@
   23.22  lemma slice_iff [iff]: "(x \<in> slice C y) = (h(x,y) \<in> C)"
   23.23    by (simp add: slice_def)
   23.24  
   23.25 -lemma slice_Union: "slice (Union S) y = (\<Union>x \<in> S. slice x y)"
   23.26 +lemma slice_Union: "slice (\<Union>S) y = (\<Union>x \<in> S. slice x y)"
   23.27    by auto
   23.28  
   23.29  lemma slice_extend_set: "slice (extend_set h A) y = A"
    24.1 --- a/src/HOL/UNITY/FP.thy	Mon Dec 28 16:34:26 2015 +0100
    24.2 +++ b/src/HOL/UNITY/FP.thy	Mon Dec 28 17:43:30 2015 +0100
    24.3 @@ -10,7 +10,7 @@
    24.4  theory FP imports UNITY begin
    24.5  
    24.6  definition FP_Orig :: "'a program => 'a set" where
    24.7 -    "FP_Orig F == Union{A. ALL B. F : stable (A Int B)}"
    24.8 +    "FP_Orig F == \<Union>{A. ALL B. F : stable (A Int B)}"
    24.9  
   24.10  definition FP :: "'a program => 'a set" where
   24.11      "FP F == {s. F : stable {s}}"
    25.1 --- a/src/HOL/UNITY/Guar.thy	Mon Dec 28 16:34:26 2015 +0100
    25.2 +++ b/src/HOL/UNITY/Guar.thy	Mon Dec 28 17:43:30 2015 +0100
    25.3 @@ -45,11 +45,11 @@
    25.4  
    25.5    (* Weakest guarantees *)
    25.6  definition wg :: "['a program, 'a program set] => 'a program set" where
    25.7 -  "wg F Y == Union({X. F \<in> X guarantees Y})"
    25.8 +  "wg F Y == \<Union>({X. F \<in> X guarantees Y})"
    25.9  
   25.10     (* Weakest existential property stronger than X *)
   25.11  definition wx :: "('a program) set => ('a program)set" where
   25.12 -   "wx X == Union({Y. Y \<subseteq> X & ex_prop Y})"
   25.13 +   "wx X == \<Union>({Y. Y \<subseteq> X & ex_prop Y})"
   25.14    
   25.15    (*Ill-defined programs can arise through "Join"*)
   25.16  definition welldef :: "'a program set" where
    26.1 --- a/src/HOL/UNITY/SubstAx.thy	Mon Dec 28 16:34:26 2015 +0100
    26.2 +++ b/src/HOL/UNITY/SubstAx.thy	Mon Dec 28 17:43:30 2015 +0100
    26.3 @@ -61,7 +61,7 @@
    26.4  done
    26.5  
    26.6  lemma LeadsTo_Union: 
    26.7 -     "(!!A. A \<in> S ==> F \<in> A LeadsTo B) ==> F \<in> (Union S) LeadsTo B"
    26.8 +     "(!!A. A \<in> S ==> F \<in> A LeadsTo B) ==> F \<in> (\<Union>S) LeadsTo B"
    26.9  apply (simp add: LeadsTo_def)
   26.10  apply (subst Int_Union)
   26.11  apply (blast intro: leadsTo_UN)
   26.12 @@ -152,7 +152,7 @@
   26.13  by (blast intro: LeadsTo_UN LeadsTo_weaken_L)
   26.14  
   26.15  lemma LeadsTo_Union_distrib:
   26.16 -     "(F \<in> (Union S) LeadsTo B)  =  (\<forall>A \<in> S. F \<in> A LeadsTo B)"
   26.17 +     "(F \<in> (\<Union>S) LeadsTo B)  =  (\<forall>A \<in> S. F \<in> A LeadsTo B)"
   26.18  by (blast intro: LeadsTo_Union LeadsTo_weaken_L)
   26.19  
   26.20  
    27.1 --- a/src/HOL/UNITY/UNITY.thy	Mon Dec 28 16:34:26 2015 +0100
    27.2 +++ b/src/HOL/UNITY/UNITY.thy	Mon Dec 28 17:43:30 2015 +0100
    27.3 @@ -48,7 +48,7 @@
    27.4      "stable A == A co A"
    27.5  
    27.6  definition strongest_rhs :: "['a program, 'a set] => 'a set" where
    27.7 -    "strongest_rhs F A == Inter {B. F \<in> A co B}"
    27.8 +    "strongest_rhs F A == \<Inter>{B. F \<in> A co B}"
    27.9  
   27.10  definition invariant :: "'a set => 'a program set" where
   27.11      "invariant A == {F. Init F \<subseteq> A} \<inter> stable A"
   27.12 @@ -343,7 +343,7 @@
   27.13  lemma Un_Diff_Diff [simp]: "A \<union> B - (A - B) = B"
   27.14  by blast
   27.15  
   27.16 -lemma Int_Union_Union: "Union(B) \<inter> A = Union((%C. C \<inter> A)`B)"
   27.17 +lemma Int_Union_Union: "\<Union>B \<inter> A = \<Union>((%C. C \<inter> A)`B)"
   27.18  by blast
   27.19  
   27.20  text{*Needed for WF reasoning in WFair.thy*}
    28.1 --- a/src/HOL/UNITY/WFair.thy	Mon Dec 28 16:34:26 2015 +0100
    28.2 +++ b/src/HOL/UNITY/WFair.thy	Mon Dec 28 17:43:30 2015 +0100
    28.3 @@ -65,7 +65,7 @@
    28.4    
    28.5  definition wlt :: "['a program, 'a set] => 'a set" where
    28.6       --{*predicate transformer: the largest set that leads to @{term B}*}
    28.7 -    "wlt F B == Union {A. F \<in> A leadsTo B}"
    28.8 +    "wlt F B == \<Union>{A. F \<in> A leadsTo B}"
    28.9  
   28.10  notation leadsTo  (infixl "\<longmapsto>" 60)
   28.11  
   28.12 @@ -189,13 +189,13 @@
   28.13  
   28.14  text{*The Union introduction rule as we should have liked to state it*}
   28.15  lemma leadsTo_Union: 
   28.16 -    "(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (Union S) leadsTo B"
   28.17 +    "(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (\<Union>S) leadsTo B"
   28.18  apply (unfold leadsTo_def)
   28.19  apply (blast intro: leads.Union)
   28.20  done
   28.21  
   28.22  lemma leadsTo_Union_Int: 
   28.23 - "(!!A. A \<in> S ==> F \<in> (A \<inter> C) leadsTo B) ==> F \<in> (Union S \<inter> C) leadsTo B"
   28.24 + "(!!A. A \<in> S ==> F \<in> (A \<inter> C) leadsTo B) ==> F \<in> (\<Union>S \<inter> C) leadsTo B"
   28.25  apply (unfold leadsTo_def)
   28.26  apply (simp only: Int_Union_Union)
   28.27  apply (blast intro: leads.Union)
   28.28 @@ -223,7 +223,7 @@
   28.29        !!A B. F \<in> A ensures B ==> P A B;  
   28.30        !!A B C. [| F \<in> A leadsTo B; P A B; F \<in> B leadsTo C; P B C |]  
   28.31                 ==> P A C;  
   28.32 -      !!B S. \<forall>A \<in> S. F \<in> A leadsTo B & P A B ==> P (Union S) B  
   28.33 +      !!B S. \<forall>A \<in> S. F \<in> A leadsTo B & P A B ==> P (\<Union>S) B  
   28.34     |] ==> P za zb"
   28.35  apply (unfold leadsTo_def)
   28.36  apply (drule CollectD, erule leads.induct)
   28.37 @@ -251,7 +251,7 @@
   28.38    "[| F \<in> za leadsTo zb;   
   28.39        P zb;  
   28.40        !!A B. [| F \<in> A ensures B;  P B |] ==> P A;  
   28.41 -      !!S. \<forall>A \<in> S. P A ==> P (Union S)  
   28.42 +      !!S. \<forall>A \<in> S. P A ==> P (\<Union>S)  
   28.43     |] ==> P za"
   28.44  txt{*by induction on this formula*}
   28.45  apply (subgoal_tac "P zb --> P za")
   28.46 @@ -265,7 +265,7 @@
   28.47    "[| F \<in> za leadsTo zb;   
   28.48        P zb;  
   28.49        !!A B. [| F \<in> A ensures B;  F \<in> B leadsTo zb;  P B |] ==> P A;  
   28.50 -      !!S. \<forall>A \<in> S. F \<in> A leadsTo zb & P A ==> P (Union S)  
   28.51 +      !!S. \<forall>A \<in> S. F \<in> A leadsTo zb & P A ==> P (\<Union>S)  
   28.52     |] ==> P za"
   28.53  apply (subgoal_tac "F \<in> za leadsTo zb & P za")
   28.54  apply (erule conjunct2)
   28.55 @@ -293,7 +293,7 @@
   28.56  by (blast intro: leadsTo_UN leadsTo_weaken_L)
   28.57  
   28.58  lemma leadsTo_Union_distrib:
   28.59 -     "F \<in> (Union S) leadsTo B  =  (\<forall>A \<in> S. F \<in> A leadsTo B)"
   28.60 +     "F \<in> (\<Union>S) leadsTo B  =  (\<forall>A \<in> S. F \<in> A leadsTo B)"
   28.61  by (blast intro: leadsTo_Union leadsTo_weaken_L)
   28.62  
   28.63  
    29.1 --- a/src/HOL/Wellfounded.thy	Mon Dec 28 16:34:26 2015 +0100
    29.2 +++ b/src/HOL/Wellfounded.thy	Mon Dec 28 17:43:30 2015 +0100
    29.3 @@ -305,7 +305,7 @@
    29.4  lemma wf_Union: 
    29.5   "[| ALL r:R. wf r;  
    29.6       ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}  
    29.7 -  |] ==> wf(Union R)"
    29.8 +  |] ==> wf (\<Union> R)"
    29.9    using wf_UN[of R "\<lambda>i. i"] by simp
   29.10  
   29.11  (*Intuition: we find an (R u S)-min element of a nonempty subset A