src/HOL/Analysis/Improper_Integral.thy

         have "(b \<bullet> i - a \<bullet> i) * (\<Sum>K\<in>snd ` S. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))
               \<le> 2 * content (cbox a b)"
         proof (rule sum_content_area_over_thin_division)
           show "snd ` S division_of \<Union>(snd ` S)"
             by (auto intro: S tagged_partial_division_of_Union_self division_of_tagged_division)
-          show "UNION S snd \<subseteq> cbox a b"
+          show "\<Union>(snd ` S) \<subseteq> cbox a b"
             using S by force
           show "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> b \<bullet> i"
             using mem_box(2) that by blast+
         qed (use that in auto)
         then show "(b \<bullet> i - a \<bullet> i) / (2 * content (cbox a b)) * (\<Sum>K\<in>snd ` S. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<le> 1"

                     and eq: "K \<inter> {x. x \<bullet> i \<le> c} = L \<inter> {x. x \<bullet> i \<le> c}"
                   have False if "K \<noteq> L"
                   proof -
                     obtain u v where uv: "L = cbox u v"
                       using T'_tagged \<open>(x, L) \<in> A\<close> \<open>A \<subseteq> T''\<close> \<open>T'' \<subseteq> T'\<close> by blast
-                    have "A tagged_division_of UNION A snd"
+                    have "A tagged_division_of \<Union>(snd ` A)"
                       using A_tagged tagged_partial_division_of_Union_self by auto
                     then have "interior (K \<inter> {x. x \<bullet> i \<le> c}) = {}"
                       apply (rule tagged_division_split_left_inj [OF _ \<open>(x,K) \<in> A\<close> \<open>(x,L) \<in> A\<close>])
                       using that eq \<open>i \<in> Basis\<close> by auto
                     then show False

                     and eq: "K \<inter> {x. c \<le> x \<bullet> i} = L \<inter> {x. c \<le> x \<bullet> i}"
                   have False if "K \<noteq> L"
                   proof -
                     obtain u v where uv: "L = cbox u v"
                       using T'_tagged \<open>(x, L) \<in> B\<close> \<open>B \<subseteq> T''\<close> \<open>T'' \<subseteq> T'\<close> by blast
-                    have "B tagged_division_of UNION B snd"
+                    have "B tagged_division_of \<Union>(snd ` B)"
                       using B_tagged tagged_partial_division_of_Union_self by auto
                     then have "interior (K \<inter> {x. c \<le> x \<bullet> i}) = {}"
                       apply (rule tagged_division_split_right_inj [OF _ \<open>(x,K) \<in> B\<close> \<open>(x,L) \<in> B\<close>])
                       using that eq \<open>i \<in> Basis\<close> by auto
                     then show False