# HG changeset patch
# User haftmann
# Date 1542881191 0
# Node ID 4b6ddc5989fca8350458c3cb008c2c73647df437
# Parent  39ba40eb2150d2e7a2cd7f4289072438161338b2
removed legacy input syntax

diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -2792,7 +2792,7 @@
     show "U ` \<F> \<subseteq> \<U>"
       using \<open>\<F> \<subseteq> \<V>\<close> U by auto
   next
-    show "f ` S \<subseteq> UNION \<F> U"
+    show "f ` S \<subseteq> \<Union> (U ` \<F>)"
       using \<F>(2-3) U UnionE subset_eq U by fastforce
   qed
 qed
diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -4991,11 +4991,11 @@
                   and ope\<phi>: "\<And>C. C \<in> components S \<Longrightarrow> openin (subtopology euclidean S) (\<phi> C)"
                   and hom\<phi>: "\<And>C. C \<in> components S \<Longrightarrow> homotopic_with (\<lambda>x. True) (\<phi> C) T f g"
       by metis
-    have Seq: "S = UNION (components S) \<phi>"
+    have Seq: "S = \<Union> (\<phi> ` components S)"
     proof
-      show "S \<subseteq> UNION (components S) \<phi>"
+      show "S \<subseteq> \<Union> (\<phi> ` components S)"
         by (metis Sup_mono Union_components \<phi> imageI)
-      show "UNION (components S) \<phi> \<subseteq> S"
+      show "\<Union> (\<phi> ` components S) \<subseteq> S"
         using ope\<phi> openin_imp_subset by fastforce
     qed
     show ?lhs
diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/Analysis/Caratheodory.thy
--- a/src/HOL/Analysis/Caratheodory.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Caratheodory.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -187,13 +187,13 @@
   case 0 show ?case using f by (simp add: positive_def)
 next
   case (Suc n)
-  have 2: "A n \<inter> UNION {0..<n} A = {}" using disj
+  have 2: "A n \<inter> \<Union> (A ` {0..<n}) = {}" using disj
     by (force simp add: disjoint_family_on_def neq_iff)
   have 3: "A n \<in> lambda_system \<Omega> M f" using A
     by blast
   interpret l: algebra \<Omega> "lambda_system \<Omega> M f"
     using f by (rule lambda_system_algebra)
-  have 4: "UNION {0..<n} A \<in> lambda_system \<Omega> M f"
+  have 4: "\<Union> (A ` {0..<n}) \<in> lambda_system \<Omega> M f"
     using A l.UNION_in_sets by simp
   from Suc.hyps show ?case
     by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4])
@@ -250,7 +250,7 @@
       fix n
       have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> M"
         by (metis A'' UNION_in_sets)
-      have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
+      have le_fa: "f (\<Union> (A ` {0..<n}) \<inter> a) \<le> f a" using A''
         by (blast intro: increasingD [OF inc] A'' UNION_in_sets)
       have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system \<Omega> M f"
         using ls.UNION_in_sets by (simp add: A)
diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -652,12 +652,12 @@
   proof (intro exI conjI)
     show "range ?DD \<subseteq> Collect compact"
       using D by clarsimp (metis mem_Collect_eq rangeI split_conv subsetCE surj_pair)
-    show "S = UNION UNIV ?DD"
+    show "S = \<Union> (range ?DD)"
     proof
-      show "S \<subseteq> UNION UNIV ?DD"
+      show "S \<subseteq> \<Union> (range ?DD)"
         using D F
         by clarsimp (metis UN_iff old.prod.case prod_decode_inverse prod_encode_eq)
-      show "UNION UNIV ?DD \<subseteq> S"
+      show "\<Union> (range ?DD) \<subseteq> S"
         using D F  by fastforce
     qed
   qed
@@ -2713,11 +2713,11 @@
     qed
     show "\<exists>T. f ` S \<subseteq> T \<and> T \<in> lmeasurable \<and> ?\<mu> T \<le> e"
     proof (intro exI conjI)
-      show "f ` S \<subseteq> UNION \<D> g"
+      show "f ` S \<subseteq> \<Union> (g ` \<D>)"
         using covers sub_g by force
-      show "UNION \<D> g \<in> lmeasurable"
+      show "\<Union> (g ` \<D>) \<in> lmeasurable"
         by (rule fmeasurable_UN_bound [OF \<open>countable \<D>\<close> meas_g le_e])
-      show "?\<mu> (UNION \<D> g) \<le> e"
+      show "?\<mu> (\<Union> (g ` \<D>)) \<le> e"
         by (rule measure_UN_bound [OF \<open>countable \<D>\<close> meas_g le_e])
     qed
   qed
@@ -3594,7 +3594,7 @@
           show "norm (integral (?U k) (norm \<circ> ?D)) \<le> integral (\<Union>n. F n) (norm \<circ> ?D)"
             unfolding integral_restrict_UNIV [of _ "norm \<circ> ?D", symmetric]
           proof (rule integral_norm_bound_integral)
-            show "(\<lambda>x. if x \<in> UNION {..k} F then (norm \<circ> ?D) x else 0) integrable_on UNIV"
+            show "(\<lambda>x. if x \<in> \<Union> (F ` {..k}) then (norm \<circ> ?D) x else 0) integrable_on UNIV"
               "(\<lambda>x. if x \<in> (\<Union>n. F n) then (norm \<circ> ?D) x else 0) integrable_on UNIV"
               using DU(1) DS
               unfolding absolutely_integrable_on_def o_def integrable_restrict_UNIV by auto
diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Connected.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -4762,7 +4762,7 @@
   moreover have "\<Union>\<D> \<subseteq> \<Union>\<F>"
     using \<D>_def by blast
   ultimately have eq1: "\<Union>\<F> = \<Union>\<D>" ..
-  have eq2: "\<Union>\<D> = UNION \<D> G"
+  have eq2: "\<Union>\<D> = \<Union> (G ` \<D>)"
     using G eq1 by auto
   show ?thesis
     apply (rule_tac \<F>' = "G ` \<D>" in that)
@@ -4781,7 +4781,7 @@
     by metis
   have [simp]: "\<And>\<F>'. \<F>' \<subseteq> \<F> \<Longrightarrow> \<Union>\<F>' = U \<inter> \<Union>(tf ` \<F>')"
     using tf by fastforce
-  obtain \<G> where "countable \<G> \<and> \<G> \<subseteq> tf ` \<F>" "\<Union>\<G> = UNION \<F> tf"
+  obtain \<G> where "countable \<G> \<and> \<G> \<subseteq> tf ` \<F>" "\<Union>\<G> = \<Union>(tf ` \<F>)"
     using tf by (force intro: Lindelof [of "tf ` \<F>"])
   then obtain \<F>' where \<F>': "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
     by (clarsimp simp add: countable_subset_image)
diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -1937,25 +1937,25 @@
   shows measurable_countable_negligible_Union: "(\<Union>n. S n) \<in> lmeasurable"
   and   measure_countable_negligible_Union:    "(\<lambda>n. (measure lebesgue (S n))) sums measure lebesgue (\<Union>n. S n)" (is ?Sums)
 proof -
-  have 1: "UNION {..n} S \<in> lmeasurable" for n
+  have 1: "\<Union> (S ` {..n}) \<in> lmeasurable" for n
     using S by blast
-  have 2: "measure lebesgue (UNION {..n} S) \<le> B" for n
+  have 2: "measure lebesgue (\<Union> (S ` {..n})) \<le> B" for n
   proof -
-    have "measure lebesgue (UNION {..n} S) \<le> (\<Sum>k\<le>n. measure lebesgue (S k))"
+    have "measure lebesgue (\<Union> (S ` {..n})) \<le> (\<Sum>k\<le>n. measure lebesgue (S k))"
       by (simp add: S fmeasurableD measure_UNION_le)
     with leB show ?thesis
       using order_trans by blast
   qed
-  have 3: "\<And>n. UNION {..n} S \<subseteq> UNION {..Suc n} S"
+  have 3: "\<And>n. \<Union> (S ` {..n}) \<subseteq> \<Union> (S ` {..Suc n})"
     by (simp add: SUP_subset_mono)
-  have eqS: "(\<Union>n. S n) = (\<Union>n. UNION {..n} S)"
+  have eqS: "(\<Union>n. S n) = (\<Union>n. \<Union> (S ` {..n}))"
     using atLeastAtMost_iff by blast
-  also have "(\<Union>n. UNION {..n} S) \<in> lmeasurable"
+  also have "(\<Union>n. \<Union> (S ` {..n})) \<in> lmeasurable"
     by (intro measurable_nested_Union [OF 1 2] 3)
   finally show "(\<Union>n. S n) \<in> lmeasurable" .
-  have eqm: "(\<Sum>i\<le>n. measure lebesgue (S i)) = measure lebesgue (UNION {..n} S)" for n
+  have eqm: "(\<Sum>i\<le>n. measure lebesgue (S i)) = measure lebesgue (\<Union> (S ` {..n}))" for n
     using assms by (simp add: measure_negligible_finite_Union_image pairwise_mono)
-  have "(\<lambda>n. (measure lebesgue (S n))) sums measure lebesgue (\<Union>n. UNION {..n} S)"
+  have "(\<lambda>n. (measure lebesgue (S n))) sums measure lebesgue (\<Union>n. \<Union> (S ` {..n}))"
     by (simp add: sums_def' eqm atLeast0AtMost) (intro measure_nested_Union [OF 1 2] 3)
   then show ?Sums
     by (simp add: eqS)
@@ -1981,7 +1981,7 @@
     using bo bounded_subset_cbox_symmetric by metis
   then have B: "(\<Sum>k\<le>n. measure lebesgue (S k)) \<le> measure lebesgue (cbox a b)" for n
   proof -
-    have "(\<Sum>k\<le>n. measure lebesgue (S k)) = measure lebesgue (UNION {..n} S)"
+    have "(\<Sum>k\<le>n. measure lebesgue (S k)) = measure lebesgue (\<Union> (S ` {..n}))"
       using measure_negligible_finite_Union_image [OF _ _ pairwise_subset] djointish
       by (metis S finite_atMost subset_UNIV)
     also have "\<dots> \<le> measure lebesgue (cbox a b)"
@@ -2024,7 +2024,7 @@
     have eq: "(\<Union>n. \<Union>k\<le>n. from_nat_into \<D> k) = (\<Union>\<D>)"
       using \<open>countable \<D>\<close> False
       by (auto intro: from_nat_into dest: from_nat_into_surj [OF \<open>countable \<D>\<close>])
-    show "measure lebesgue (\<Union>\<D>) - e < measure lebesgue (UNION {..N} (from_nat_into \<D>))"
+    show "measure lebesgue (\<Union>\<D>) - e < measure lebesgue (\<Union> (from_nat_into \<D> ` {..N}))"
       using N [OF order_refl]
       by (auto simp: eq algebra_simps dist_norm)
   qed auto
@@ -2779,9 +2779,9 @@
         by (simp add: False \<D>(1) from_nat_into infinite_imp_nonempty negl_int)
       have TB: "(\<Sum>k\<le>n. ?\<mu> (?T k)) \<le> ?\<mu> S + e" for n
       proof -
-        have "(\<Sum>k\<le>n. ?\<mu> (?T k)) = ?\<mu> (UNION {..n} ?T)"
+        have "(\<Sum>k\<le>n. ?\<mu> (?T k)) = ?\<mu> (\<Union> (?T ` {..n}))"
           by (simp add: pairwise_def TM TN measure_negligible_finite_Union_image)
-        also have "?\<mu> (UNION {..n} ?T) \<le> ?\<mu> S + e"
+        also have "?\<mu> (\<Union> (?T ` {..n})) \<le> ?\<mu> S + e"
           using fincase [of "?T ` {..n}"] T by (auto simp: bij_betw_def)
         finally show ?thesis .
       qed
diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/Analysis/Improper_Integral.thy
--- a/src/HOL/Analysis/Improper_Integral.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Improper_Integral.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -398,11 +398,11 @@
   qed
   also have "... \<le> ?rhs"
   proof (rule subadditive_content_division)
-    show "extend ` \<D> division_of UNION \<D> extend"
+    show "extend ` \<D> division_of \<Union> (extend ` \<D>)"
       using int_extend_disjoint apply (auto simp: division_of_def \<open>finite \<D>\<close> extend)
       using extend_def apply blast
       done
-    show "UNION \<D> extend \<subseteq> cbox a b"
+    show "\<Union> (extend ` \<D>) \<subseteq> cbox a b"
       using extend by fastforce
   qed
   finally show ?thesis .
diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Starlike.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -5128,7 +5128,7 @@
               by auto
           next
             assume "N - X \<subseteq> N - J"
-            with J have "N - X \<union> UNION \<H> ((-) N) \<subseteq> N - J"
+            with J have "N - X \<union> \<Union> ((-) N ` \<H>) \<subseteq> N - J"
               by auto
             with \<open>J \<in> \<H>\<close> show ?thesis
               by blast
@@ -7920,7 +7920,7 @@
       finally show "closure (\<Union>x\<in>- S. \<Union>y\<in>ball 0 (1 / (2 + real n)). {x + y})
                     \<subseteq> (\<Union>x \<in> -S. \<Union>y\<in>ball 0 (1 / (1 + real n)). {x + y})" .
     qed
-    have "S \<subseteq> UNION UNIV ?C"
+    have "S \<subseteq> \<Union> (range ?C)"
     proof
       fix x
       assume x: "x \<in> S"
@@ -7947,10 +7947,10 @@
         with that show ?thesis
           by auto
       qed
-      with N2 show "x \<in> UNION UNIV ?C"
+      with N2 show "x \<in> \<Union> (range ?C)"
         by (rule_tac a = "N1+N2" in UN_I) (auto simp: dist_norm norm_minus_commute)
     qed
-    then show "UNION UNIV ?C = S" by auto
+    then show "\<Union> (range ?C) = S" by auto
   qed
   ultimately show ?thesis
     using that by metis
diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -448,11 +448,11 @@
           by (intro exI[of _ "{i \<union> j| i j.  i \<in> x \<and> j \<in> y}"]) (auto dest: x(2) y(2))
       next
         case (UN K)
-        then have "\<forall>k\<in>K. \<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = k" by auto
+        then have "\<forall>k\<in>K. \<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. \<Union> (Inter ` B') = k" by auto
         then obtain k where
             "\<forall>ka\<in>K. k ka \<subseteq> {b. finite b \<and> b \<subseteq> B} \<and> \<Union>(Inter ` (k ka)) = ka"
           unfolding bchoice_iff ..
-        then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = \<Union>K"
+        then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. \<Union> (Inter ` B') = \<Union>K"
           by (intro exI[of _ "\<Union>(k ` K)"]) auto
       next
         case (Basis S)
diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -3378,8 +3378,8 @@
   (is "?l = ?r")
 proof -
   let ?KM = "{(k,m). k + m \<le> n}"
-  let ?f = "\<lambda>s. UNION {(0::nat)..s} (\<lambda>i. {(i,s - i)})"
-  have th0: "?KM = UNION {0..n} ?f"
+  let ?f = "\<lambda>s. \<Union>i\<in>{0..s}. {(i, s - i)}"
+  have th0: "?KM = \<Union> (?f ` {0..n})"
     by auto
   show "?l = ?r "
     unfolding th0
diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Decision_Procs/MIR.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -7,6 +7,12 @@
   "HOL-Library.Code_Target_Numeral" "HOL-Library.Old_Recdef"
 begin
 
+section \<open>Prelude\<close>
+
+abbreviation (input) UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
+  where "UNION A f \<equiv> \<Union> (f ` A)" \<comment> \<open>legacy\<close>
+
+
 section \<open>Quantifier elimination for \<open>\<real> (0, 1, +, floor, <)\<close>\<close>
 
 declare of_int_floor_cancel [simp del]
diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/Library/Countable_Set_Type.thy
--- a/src/HOL/Library/Countable_Set_Type.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Library/Countable_Set_Type.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -440,7 +440,7 @@
 
 lemma rel_cset_cUNION:
   "\<lbrakk> rel_cset Q A B; rel_fun Q (rel_cset R) f g \<rbrakk>
-  \<Longrightarrow> rel_cset R (cUNION A f) (cUNION B g)"
+  \<Longrightarrow> rel_cset R (cUnion (cimage f A)) (cUnion (cimage g B))"
 unfolding rel_fun_def by transfer(erule rel_set_UNION, simp add: rel_fun_def)
 
 lemma rel_cset_csingle_iff [simp]: "rel_cset R (csingle x) (csingle y) \<longleftrightarrow> R x y"
diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/Library/Set_Idioms.thy
--- a/src/HOL/Library/Set_Idioms.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Library/Set_Idioms.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -375,9 +375,9 @@
       using R unfolding relative_to_def union_of_def by auto
     then obtain f where f: "\<And>T. T \<in> \<U> \<Longrightarrow> P (f T)" "\<And>T. T \<in> \<U> \<Longrightarrow> U \<inter> (f T) = T"
       by metis
-    then have "\<exists>\<U>'\<subseteq>Collect P. \<Union>\<U>' = UNION \<U> f"
+    then have "\<exists>\<U>'\<subseteq>Collect P. \<Union>\<U>' = \<Union> (f ` \<U>)"
       by (metis image_subset_iff mem_Collect_eq)
-    moreover have eq: "U \<inter> UNION \<U> f = \<Union>\<U>"
+    moreover have eq: "U \<inter> \<Union> (f ` \<U>) = \<Union>\<U>"
       using f by auto
     ultimately show ?thesis
       unfolding relative_to_def union_of_def arbitrary_def \<open>S = \<Union>\<U>\<close>
@@ -404,14 +404,14 @@
       using R unfolding relative_to_def union_of_def by auto
     then obtain f where f: "\<And>T. T \<in> \<U> \<Longrightarrow> P (f T)" "\<And>T. T \<in> \<U> \<Longrightarrow> U \<inter> (f T) = T"
       by metis
-    then have "\<exists>\<U>'\<subseteq>Collect P. \<Union>\<U>' = UNION \<U> f"
+    then have "\<exists>\<U>'\<subseteq>Collect P. \<Union>\<U>' = \<Union> (f ` \<U>)"
       by (metis image_subset_iff mem_Collect_eq)
-    moreover have eq: "U \<inter> UNION \<U> f = \<Union>\<U>"
+    moreover have eq: "U \<inter> \<Union> (f ` \<U>) = \<Union>\<U>"
       using f by auto
     ultimately show ?thesis
       using \<open>finite \<U>\<close> f
       unfolding relative_to_def union_of_def \<open>S = \<Union>\<U>\<close>
-      by (rule_tac x="UNION \<U> f" in exI) (metis finite_imageI image_subsetI mem_Collect_eq)
+      by (rule_tac x="\<Union> (f ` \<U>)" in exI) (metis finite_imageI image_subsetI mem_Collect_eq)
   qed
   ultimately show ?thesis
     by blast
@@ -434,14 +434,14 @@
       using R unfolding relative_to_def union_of_def by auto
     then obtain f where f: "\<And>T. T \<in> \<U> \<Longrightarrow> P (f T)" "\<And>T. T \<in> \<U> \<Longrightarrow> U \<inter> (f T) = T"
       by metis
-    then have "\<exists>\<U>'\<subseteq>Collect P. \<Union>\<U>' = UNION \<U> f"
+    then have "\<exists>\<U>'\<subseteq>Collect P. \<Union>\<U>' = \<Union> (f ` \<U>)"
       by (metis image_subset_iff mem_Collect_eq)
-    moreover have eq: "U \<inter> UNION \<U> f = \<Union>\<U>"
+    moreover have eq: "U \<inter> \<Union> (f ` \<U>) = \<Union>\<U>"
       using f by auto
     ultimately show ?thesis
       using \<open>countable \<U>\<close> f
       unfolding relative_to_def union_of_def \<open>S = \<Union>\<U>\<close>
-      by (rule_tac x="UNION \<U> f" in exI) (metis countable_image image_subsetI mem_Collect_eq)
+      by (rule_tac x="\<Union> (f ` \<U>)" in exI) (metis countable_image image_subsetI mem_Collect_eq)
   qed
   ultimately show ?thesis
     by blast
diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Probability/Independent_Family.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -611,15 +611,15 @@
   unfolding indep_vars_def2 by (intro conj_cong indep_sets_cong) auto
 
 definition (in prob_space) tail_events where
-  "tail_events A = (\<Inter>n. sigma_sets (space M) (UNION {n..} A))"
+  "tail_events A = (\<Inter>n. sigma_sets (space M) (\<Union> (A ` {n..})))"
 
 lemma (in prob_space) tail_events_sets:
   assumes A: "\<And>i::nat. A i \<subseteq> events"
   shows "tail_events A \<subseteq> events"
 proof
   fix X assume X: "X \<in> tail_events A"
-  let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))"
-  from X have "\<And>n::nat. X \<in> sigma_sets (space M) (UNION {n..} A)" by (auto simp: tail_events_def)
+  let ?A = "(\<Inter>n. sigma_sets (space M) (\<Union> (A ` {n..})))"
+  from X have "\<And>n::nat. X \<in> sigma_sets (space M) (\<Union> (A ` {n..}))" by (auto simp: tail_events_def)
   from this[of 0] have "X \<in> sigma_sets (space M) (\<Union>(A ` UNIV))" by simp
   then show "X \<in> events"
     by induct (insert A, auto)
@@ -630,16 +630,16 @@
   shows "sigma_algebra (space M) (tail_events A)"
   unfolding tail_events_def
 proof (simp add: sigma_algebra_iff2, safe)
-  let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))"
+  let ?A = "(\<Inter>n. sigma_sets (space M) (\<Union> (A ` {n..})))"
   interpret A: sigma_algebra "space M" "A i" for i by fact
   { fix X x assume "X \<in> ?A" "x \<in> X"
-    then have "\<And>n. X \<in> sigma_sets (space M) (UNION {n..} A)" by auto
+    then have "\<And>n. X \<in> sigma_sets (space M) (\<Union> (A ` {n..}))" by auto
     from this[of 0] have "X \<in> sigma_sets (space M) (\<Union>(A ` UNIV))" by simp
     then have "X \<subseteq> space M"
       by induct (insert A.sets_into_space, auto)
     with \<open>x \<in> X\<close> show "x \<in> space M" by auto }
   { fix F :: "nat \<Rightarrow> 'a set" and n assume "range F \<subseteq> ?A"
-    then show "(\<Union>(F ` UNIV)) \<in> sigma_sets (space M) (UNION {n..} A)"
+    then show "(\<Union>(F ` UNIV)) \<in> sigma_sets (space M) (\<Union> (A ` {n..}))"
       by (intro sigma_sets.Union) auto }
 qed (auto intro!: sigma_sets.Compl sigma_sets.Empty)
 
diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -99,7 +99,7 @@
   client_allowed_acts :: "'a clientState_d program set"
   where "client_allowed_acts =
        {F. AllowedActs F =
-            insert Id (UNION (preserves (funPair rel ask)) Acts)}"
+            insert Id (\<Union> (Acts ` preserves (funPair rel ask)))}"
 
 definition
   client_spec :: "'a clientState_d program set"
@@ -208,11 +208,9 @@
   \<comment> \<open>environmental constraints\<close>
   network_allowed_acts :: "'a systemState program set"
   where "network_allowed_acts =
-       {F. AllowedActs F =
-           insert Id
-            (UNION (preserves allocRel Int
-                    (INT i: lessThan Nclients. preserves(giv o sub i o client)))
-                  Acts)}"
+       {F. AllowedActs F = insert Id
+         (\<Union> (Acts ` (preserves allocRel \<inter> (\<Inter>i<Nclients.
+           preserves (giv \<circ> sub i \<circ> client)))))}"
 
 definition
   network_spec :: "'a systemState program set"
diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/UNITY/Comp/AllocImpl.thy
--- a/src/HOL/UNITY/Comp/AllocImpl.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -92,7 +92,7 @@
   merge_allowed_acts :: "('a,'b) merge_d program set"
   where "merge_allowed_acts =
        {F. AllowedActs F =
-            insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}"
+            insert Id (\<Union> (Acts ` preserves (funPair merge.Out iOut)))}"
 
 definition
   merge_spec :: "('a,'b) merge_d program set"