# HG changeset patch
# User nipkow
# Date 1548667667 -3600
# Node ID aec42cee2521464873b2af232f4cd44067a0e734
# Parent  bb0a354f6b462bb29530a71958775296aeacaa8b
more canonical and less specialized syntax

diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -3090,7 +3090,7 @@
   assume \<U>: "Ball \<U> (openin X) \<and> C \<subseteq> \<Union>\<U>"
   have "(\<forall>U\<in>insert (topspace X - C) \<U>. openin X U)"
     using XC \<U> by blast
-  moreover have "K \<subseteq> \<Union>insert (topspace X - C) \<U>"
+  moreover have "K \<subseteq> \<Union>(insert (topspace X - C) \<U>)"
     using \<U> XK compactin_subset_topspace by fastforce
   ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> insert (topspace X - C) \<U>" "K \<subseteq> \<Union>\<F>"
     using assms unfolding compactin_def by metis
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Analysis/Arcwise_Connected.thy
--- a/src/HOL/Analysis/Arcwise_Connected.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Arcwise_Connected.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -13,7 +13,7 @@
 theorem Brouwer_reduction_theorem_gen:
   fixes S :: "'a::euclidean_space set"
   assumes "closed S" "\<phi> S"
-      and \<phi>: "\<And>F. \<lbrakk>\<And>n. closed(F n); \<And>n. \<phi>(F n); \<And>n. F(Suc n) \<subseteq> F n\<rbrakk> \<Longrightarrow> \<phi>(\<Inter>range F)"
+      and \<phi>: "\<And>F. \<lbrakk>\<And>n. closed(F n); \<And>n. \<phi>(F n); \<And>n. F(Suc n) \<subseteq> F n\<rbrakk> \<Longrightarrow> \<phi>(\<Inter>(range F))"
   obtains T where "T \<subseteq> S" "closed T" "\<phi> T" "\<And>U. \<lbrakk>U \<subseteq> S; closed U; \<phi> U\<rbrakk> \<Longrightarrow> \<not> (U \<subset> T)"
 proof -
   obtain B :: "nat \<Rightarrow> 'a set"
@@ -36,7 +36,7 @@
     by (induction n) (auto simp: assms ASuc dest!: someI_ex)
   show ?thesis
   proof
-    show "\<Inter>range A \<subseteq> S"
+    show "\<Inter>(range A) \<subseteq> S"
       using \<open>\<And>n. A n \<subseteq> S\<close> by blast
     show "closed (\<Inter>(A ` UNIV))"
       using clo by blast
@@ -81,7 +81,7 @@
 corollary Brouwer_reduction_theorem:
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" "\<phi> S" "S \<noteq> {}"
-      and \<phi>: "\<And>F. \<lbrakk>\<And>n. compact(F n); \<And>n. F n \<noteq> {}; \<And>n. \<phi>(F n); \<And>n. F(Suc n) \<subseteq> F n\<rbrakk> \<Longrightarrow> \<phi>(\<Inter>range F)"
+      and \<phi>: "\<And>F. \<lbrakk>\<And>n. compact(F n); \<And>n. F n \<noteq> {}; \<And>n. \<phi>(F n); \<And>n. F(Suc n) \<subseteq> F n\<rbrakk> \<Longrightarrow> \<phi>(\<Inter>(range F))"
   obtains T where "T \<subseteq> S" "compact T" "T \<noteq> {}" "\<phi> T"
                   "\<And>U. \<lbrakk>U \<subseteq> S; closed U; U \<noteq> {}; \<phi> U\<rbrakk> \<Longrightarrow> \<not> (U \<subset> T)"
 proof (rule Brouwer_reduction_theorem_gen [of S "\<lambda>T. T \<noteq> {} \<and> T \<subseteq> S \<and> \<phi> T"])
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -529,7 +529,7 @@
     from ex_countable_basis obtain B :: "'a set set" where
       B:  "\<And>b. b \<in> B \<Longrightarrow> open b" "\<And>X. open X \<Longrightarrow> \<exists>b\<subseteq>B. (\<Union>b) = X" and "countable B"
       by (auto simp: topological_basis_def)
-    from B(2)[OF K] obtain m where m: "\<And>k. k \<in> K \<Longrightarrow> m k \<subseteq> B" "\<And>k. k \<in> K \<Longrightarrow> (\<Union>m k) = k"
+    from B(2)[OF K] obtain m where m: "\<And>k. k \<in> K \<Longrightarrow> m k \<subseteq> B" "\<And>k. k \<in> K \<Longrightarrow> \<Union>(m k) = k"
       by metis
     define U where "U = (\<Union>k\<in>K. m k)"
     with m have "countable U"
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Analysis/Caratheodory.thy
--- a/src/HOL/Analysis/Caratheodory.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Caratheodory.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -550,7 +550,7 @@
   then show "\<mu> (\<Union>C) = sum \<mu> C"
   proof (induct C)
     case (insert c C)
-    from insert(1,2,4,5) have "\<mu> (\<Union>insert c C) = \<mu> c + \<mu> (\<Union>C)"
+    from insert(1,2,4,5) have "\<mu> (\<Union>(insert c C)) = \<mu> c + \<mu> (\<Union>C)"
       by (auto intro!: add simp: disjoint_def)
     with insert show ?case
       by (simp add: disjoint_def)
@@ -712,7 +712,7 @@
       from A C' \<open>c \<in> C'\<close> have UN_eq: "(\<Union>i. A i) = c"
         by (auto simp: A_def)
 
-      have "\<forall>i::nat. \<exists>f::nat \<Rightarrow> 'a set. \<mu>_r (A i) = (\<Sum>j. \<mu>_r (f j)) \<and> disjoint_family f \<and> \<Union>range f = A i \<and> (\<forall>j. f j \<in> M)"
+      have "\<forall>i::nat. \<exists>f::nat \<Rightarrow> 'a set. \<mu>_r (A i) = (\<Sum>j. \<mu>_r (f j)) \<and> disjoint_family f \<and> \<Union>(range f) = A i \<and> (\<forall>j. f j \<in> M)"
         (is "\<forall>i. ?P i")
       proof
         fix i
@@ -735,7 +735,7 @@
         moreover
         have Ai_eq: "A i = (\<Union>x<card C. f x)"
           using f C Ai unfolding bij_betw_def by auto
-        then have "\<Union>range f = A i"
+        then have "\<Union>(range f) = A i"
           using f C Ai unfolding bij_betw_def
             by (auto simp add: f_def cong del: SUP_cong_simp)
         moreover
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -457,7 +457,7 @@
     ultimately show ?thesis
       by (rule *)
   qed
-  then have "open (f ` \<Union>components U)"
+  then have "open (f ` \<Union>(components U))"
     by (metis (no_types, lifting) imageE image_Union open_Union)
   then show ?thesis
     by force
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Analysis/Elementary_Normed_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -898,7 +898,7 @@
 lemma compact_nest:
   fixes F :: "'a::linorder \<Rightarrow> 'b::heine_borel set"
   assumes F: "\<And>n. compact(F n)" "\<And>n. F n \<noteq> {}" and mono: "\<And>m n. m \<le> n \<Longrightarrow> F n \<subseteq> F m"
-  shows "\<Inter>range F \<noteq> {}"
+  shows "\<Inter>(range F) \<noteq> {}"
 proof -
   have *: "\<And>S T. S \<in> range F \<and> T \<in> range F \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
     by (metis mono image_iff le_cases)
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -2248,7 +2248,7 @@
       using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>(a`D)"] conjI) (auto intro!: open_INT)
   qed
   then obtain a d where a: "\<And>x. x\<in>s \<Longrightarrow> open (a x)" "s \<subseteq> (\<Union>x\<in>s. a x)"
-    and d: "\<And>x. x \<in> s \<Longrightarrow> d x \<subseteq> C \<and> finite (d x) \<and> a x \<times> t \<subseteq> \<Union>d x"
+    and d: "\<And>x. x \<in> s \<Longrightarrow> d x \<subseteq> C \<and> finite (d x) \<and> a x \<times> t \<subseteq> \<Union>(d x)"
     unfolding subset_eq UN_iff by metis
   moreover
   from compactE_image[OF \<open>compact s\<close> a]
@@ -2258,9 +2258,9 @@
   {
     from s have "s \<times> t \<subseteq> (\<Union>x\<in>e. a x \<times> t)"
       by auto
-    also have "\<dots> \<subseteq> (\<Union>x\<in>e. \<Union>d x)"
+    also have "\<dots> \<subseteq> (\<Union>x\<in>e. \<Union>(d x))"
       using d \<open>e \<subseteq> s\<close> by (intro UN_mono) auto
-    finally have "s \<times> t \<subseteq> (\<Union>x\<in>e. \<Union>d x)" .
+    finally have "s \<times> t \<subseteq> (\<Union>x\<in>e. \<Union>(d x))" .
   }
   ultimately show "\<exists>C'\<subseteq>C. finite C' \<and> s \<times> t \<subseteq> \<Union>C'"
     by (intro exI[of _ "(\<Union>x\<in>e. d x)"]) (auto simp: subset_eq)
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Analysis/Finite_Product_Measure.thy
--- a/src/HOL/Analysis/Finite_Product_Measure.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -970,7 +970,7 @@
 
   obtain F where F: "\<And>j. countable (F j)" "\<And>j f. f \<in> F j \<Longrightarrow> f \<in> sets (M j)"
     "\<And>j f. f \<in> F j \<Longrightarrow> emeasure (M j) f \<noteq> \<infinity>" and
-    in_space: "\<And>j. space (M j) = (\<Union>F j)"
+    in_space: "\<And>j. space (M j) = \<Union>(F j)"
     using sigma_finite_countable by (metis subset_eq)
   moreover have "(\<Union>(Pi\<^sub>E I ` Pi\<^sub>E I F)) = space (Pi\<^sub>M I M)"
     using in_space by (auto simp: space_PiM PiE_iff intro!: PiE_choice[THEN iffD2])
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -671,7 +671,7 @@
       let ?U = "\<lambda>j. U j \<inter> (if j = i then V else topspace(X j))"
       show ?case
       proof (intro exI conjI)
-        show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>insert F \<F> = Pi\<^sub>E I ?U"
+        show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>(insert F \<F>) = Pi\<^sub>E I ?U"
         using eq  PiE_mem \<open>i \<in> I\<close>  by (auto simp: \<open>F = {f. f i \<in> V}\<close>) fastforce
       next
         show "finite {i \<in> I. ?U i \<noteq> topspace (X i)}"
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -655,11 +655,11 @@
         using contf apply (force simp: elim: continuous_on_subset)
         using contg apply (force simp: elim: continuous_on_subset)
         using fh gh insert.hyps pwX by fastforce
-    then show "continuous_on (\<Union>insert X \<F> - insert a C) (\<lambda>a. if a \<in> X then f a else g a)"
+    then show "continuous_on (\<Union>(insert X \<F>) - insert a C) (\<lambda>a. if a \<in> X then f a else g a)"
       by (blast intro: continuous_on_subset)
-    show "\<forall>x\<in>(\<Union>insert X \<F> - insert a C) \<inter> K. (if x \<in> X then f x else g x) = h x"
+    show "\<forall>x\<in>(\<Union>(insert X \<F>) - insert a C) \<inter> K. (if x \<in> X then f x else g x) = h x"
       using gh by (auto simp: fh)
-    show "(\<lambda>a. if a \<in> X then f a else g a) ` (\<Union>insert X \<F> - insert a C) \<subseteq> T"
+    show "(\<lambda>a. if a \<in> X then f a else g a) ` (\<Union>(insert X \<F>) - insert a C) \<subseteq> T"
       using fim gim by auto force
   qed
 qed
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Polytope.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -468,28 +468,28 @@
       by (simp add: aff_dim_le_DIM)
   next
     case (Suc n)
-    have fs: "\<Inter>d (Suc n) face_of S"
+    have fs: "\<Inter>(d (Suc n)) face_of S"
       by (meson Suc.prems cfaI dn_le_Suc dn_notempty face_of_Inter subsetCE)
-    have condn: "convex (\<Inter>d n)"
+    have condn: "convex (\<Inter>(d n))"
       using Suc.prems nat_le_linear not_less_eq_eq
       by (blast intro: face_of_imp_convex cfaI convex_Inter dest: dn_le_Suc)
-    have fdn: "\<Inter>d (Suc n) face_of \<Inter>d n"
+    have fdn: "\<Inter>(d (Suc n)) face_of \<Inter>(d n)"
       by (metis (no_types, lifting) Inter_anti_mono Suc.prems dSuc cfaI dn_le_Suc dn_notempty face_of_Inter face_of_imp_subset face_of_subset subset_iff subset_insertI)
-    have ne: "\<Inter>d (Suc n) \<noteq> \<Inter>d n"
+    have ne: "\<Inter>(d (Suc n)) \<noteq> \<Inter>(d n)"
       by (metis (no_types, lifting) Suc.prems Suc_leD c complete_lattice_class.Inf_insert dSuc dn_le_Suc less_irrefl order.trans)
     have *: "\<And>m::int. \<And>d. \<And>d'::int. d < d' \<and> d' \<le> m - n \<Longrightarrow> d \<le> m - of_nat(n+1)"
       by arith
-    have "aff_dim (\<Inter>d (Suc n)) < aff_dim (\<Inter>d n)"
+    have "aff_dim (\<Inter>(d (Suc n))) < aff_dim (\<Inter>(d n))"
       by (rule face_of_aff_dim_lt [OF condn fdn ne])
-    moreover have "aff_dim (\<Inter>d n) \<le> int (DIM('a)) - int n"
+    moreover have "aff_dim (\<Inter>(d n)) \<le> int (DIM('a)) - int n"
       using Suc by auto
     ultimately
-    have "aff_dim (\<Inter>d (Suc n)) \<le> int (DIM('a)) - (n+1)" by arith
+    have "aff_dim (\<Inter>(d (Suc n))) \<le> int (DIM('a)) - (n+1)" by arith
     then show ?case by linarith
   qed
-  have "aff_dim (\<Inter>d (DIM('a) + 2)) \<le> -2"
+  have "aff_dim (\<Inter>(d (DIM('a) + 2))) \<le> -2"
       using aff_dim_le [OF order_refl] by simp
-  with aff_dim_geq [of "\<Inter>d (DIM('a) + 2)"] show ?thesis
+  with aff_dim_geq [of "\<Inter>(d (DIM('a) + 2))"] show ?thesis
     using order.trans by fastforce
 next
   case False
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Analysis/Radon_Nikodym.thy
--- a/src/HOL/Analysis/Radon_Nikodym.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Radon_Nikodym.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -837,7 +837,7 @@
     show "range (\<lambda>(i, j). A i \<inter> Q j) \<subseteq> sets (density M f)"
       using A_in_sets by auto
   next
-    have "\<Union>range (\<lambda>(i, j). A i \<inter> Q j) = (\<Union>i j. A i \<inter> Q j)"
+    have "\<Union>(range (\<lambda>(i, j). A i \<inter> Q j)) = (\<Union>i j. A i \<inter> Q j)"
       by auto
     also have "\<dots> = (\<Union>i. A i) \<inter> space M" using Q by auto
     also have "(\<Union>i. A i) = space M"
@@ -856,7 +856,7 @@
           using x real by (auto simp: A_def ennreal_of_nat_eq_real_of_nat intro!: exI[of _ "Suc n"])
       qed
     qed (auto simp: A_def)
-    finally show "\<Union>range (\<lambda>(i, j). A i \<inter> Q j) = space ?N" by simp
+    finally show "\<Union>(range (\<lambda>(i, j). A i \<inter> Q j)) = space ?N" by simp
   next
     fix X assume "X \<in> range (\<lambda>(i, j). A i \<inter> Q j)"
     then obtain i j where [simp]:"X = A i \<inter> Q j" by auto
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -4866,7 +4866,7 @@
     let ?\<C> = "insert (U \<union> V) ((\<lambda>S. N - S) ` \<F>)"
     obtain \<D> where "\<D> \<subseteq> ?\<C>" "finite \<D>" "K \<subseteq> \<Union>\<D>"
     proof (rule compactE [OF \<open>compact K\<close>])
-      show "K \<subseteq> \<Union>insert (U \<union> V) ((-) N ` \<F>)"
+      show "K \<subseteq> \<Union>(insert (U \<union> V) ((-) N ` \<F>))"
         using \<open>K \<subseteq> N\<close> ABeq \<open>A \<subseteq> U\<close> \<open>B \<subseteq> V\<close> by auto
       show "\<And>B. B \<in> insert (U \<union> V) ((-) N ` \<F>) \<Longrightarrow> open B"
         by (auto simp:  \<open>open U\<close> \<open>open V\<close> open_Un \<open>open N\<close> cc compact_imp_closed open_Diff)
@@ -6818,7 +6818,7 @@
     by metis
   obtain K where K: "closed K" "U \<inter> K = S"
     using cin by (auto simp: closedin_closed)
-  have 1: "U \<subseteq> \<Union>insert (- K) (F ` \<C>)"
+  have 1: "U \<subseteq> \<Union>(insert (- K) (F ` \<C>))"
     by clarsimp (metis Int_iff Union_iff \<open>U \<inter> K = S\<close> \<open>S \<subseteq> \<Union>\<C>\<close> subsetD intF)
   have 2: "\<And>T. T \<in> insert (- K) (F ` \<C>) \<Longrightarrow> open T"
     using \<open>closed K\<close> by (auto simp: opF)
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -633,7 +633,7 @@
   qed
   obtain q where q: "\<And>x. x \<in> p \<Longrightarrow> q x division_of cbox a b" "\<And>x. x \<in> p \<Longrightarrow> x \<in> q x"
     using bchoice[OF div_cbox] by blast
-  have "q x division_of \<Union>q x" if x: "x \<in> p" for x
+  have "q x division_of \<Union>(q x)" if x: "x \<in> p" for x
     apply (rule division_ofI)
     using division_ofD[OF q(1)[OF x]] by auto
   then have di: "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
@@ -736,7 +736,7 @@
   assumes "finite f"
     and "\<And>p. p \<in> f \<Longrightarrow> p division_of (\<Union>p)"
     and "\<And>k1 k2. k1 \<in> \<Union>f \<Longrightarrow> k2 \<in> \<Union>f \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
-  shows "\<Union>f division_of \<Union>\<Union>f"
+  shows "\<Union>f division_of \<Union>(\<Union>f)"
   using assms  by (auto intro!: division_ofI)
 
 lemma elementary_union_interval:
@@ -781,7 +781,7 @@
         by auto
       show "finite ?D"
         using "*" pdiv(1) q(1) by auto
-      have "\<Union>?D = (\<Union>x\<in>p. \<Union>insert (cbox a b) (q x))"
+      have "\<Union>?D = (\<Union>x\<in>p. \<Union>(insert (cbox a b) (q x)))"
         by auto
       also have "... = \<Union>{cbox a b \<union> t |t. t \<in> p}"
         using q(6) by auto
@@ -847,7 +847,7 @@
     from assms(2)[OF as(4)] obtain a b where x: "x = cbox a b" by blast
     have *: "\<Union>F = \<Union>p"
       using division_ofD[OF p] by auto
-    show "\<exists>p. p division_of \<Union>insert x F"
+    show "\<exists>p. p division_of \<Union>(insert x F)"
       using elementary_union_interval[OF p[unfolded *], of a b]
       unfolding Union_insert x * by metis
   qed (insert assms, auto)
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/BNF_Composition.thy
--- a/src/HOL/BNF_Composition.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/BNF_Composition.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -75,7 +75,7 @@
 lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
   by blast
 
-lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
+lemma comp_set_bd_Union_o_collect: "|\<Union>(\<Union>((\<lambda>f. f x) ` X))| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
   by (unfold comp_apply collect_def) simp
 
 lemma Collect_inj: "Collect P = Collect Q \<Longrightarrow> P = Q"
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Complete_Lattices.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -15,10 +15,10 @@
 subsection \<open>Syntactic infimum and supremum operations\<close>
 
 class Inf =
-  fixes Inf :: "'a set \<Rightarrow> 'a"  ("\<Sqinter> _" [900] 900)
+  fixes Inf :: "'a set \<Rightarrow> 'a"  ("\<Sqinter>")
 
 class Sup =
-  fixes Sup :: "'a set \<Rightarrow> 'a"  ("\<Squnion> _" [900] 900)
+  fixes Sup :: "'a set \<Rightarrow> 'a"  ("\<Squnion>")
 
 syntax (ASCII)
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
@@ -40,10 +40,10 @@
 
 translations
   "\<Sqinter>x y. f"   \<rightleftharpoons> "\<Sqinter>x. \<Sqinter>y. f"
-  "\<Sqinter>x. f"     \<rightleftharpoons> "\<Sqinter>CONST range (\<lambda>x. f)"
+  "\<Sqinter>x. f"     \<rightleftharpoons> "\<Sqinter>(CONST range (\<lambda>x. f))"
   "\<Sqinter>x\<in>A. f"   \<rightleftharpoons> "CONST Inf ((\<lambda>x. f) ` A)"
   "\<Squnion>x y. f"   \<rightleftharpoons> "\<Squnion>x. \<Squnion>y. f"
-  "\<Squnion>x. f"     \<rightleftharpoons> "\<Squnion>CONST range (\<lambda>x. f)"
+  "\<Squnion>x. f"     \<rightleftharpoons> "\<Squnion>(CONST range (\<lambda>x. f))"
   "\<Squnion>x\<in>A. f"   \<rightleftharpoons> "CONST Sup ((\<lambda>x. f) `  A)"
 
 context Inf
@@ -175,13 +175,13 @@
 lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<le> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<le> u)"
   using Sup_le_iff [of "f ` A"] by simp
 
-lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
+lemma Inf_insert [simp]: "\<Sqinter>(insert a A) = a \<sqinter> \<Sqinter>A"
   by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
 
 lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> \<Sqinter>(f ` A)"
   by (simp cong del: INF_cong_simp)
 
-lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
+lemma Sup_insert [simp]: "\<Squnion>(insert a A) = a \<squnion> \<Squnion>A"
   by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
 
 lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> \<Squnion>(f ` A)"
@@ -779,7 +779,7 @@
 
 subsubsection \<open>Inter\<close>
 
-abbreviation Inter :: "'a set set \<Rightarrow> 'a set"  ("\<Inter> _" [900] 900)
+abbreviation Inter :: "'a set set \<Rightarrow> 'a set"  ("\<Inter>")
   where "\<Inter>S \<equiv> \<Sqinter>S"
 
 lemma Inter_eq: "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
@@ -860,7 +860,7 @@
 
 translations
   "\<Inter>x y. f"  \<rightleftharpoons> "\<Inter>x. \<Inter>y. f"
-  "\<Inter>x. f"    \<rightleftharpoons> "\<Inter>CONST range (\<lambda>x. f)"
+  "\<Inter>x. f"    \<rightleftharpoons> "\<Inter>(CONST range (\<lambda>x. f))"
   "\<Inter>x\<in>A. f"  \<rightleftharpoons> "CONST Inter ((\<lambda>x. f) ` A)"
 
 lemma INTER_eq: "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
@@ -933,7 +933,7 @@
 
 subsubsection \<open>Union\<close>
 
-abbreviation Union :: "'a set set \<Rightarrow> 'a set"  ("\<Union> _" [900] 900)
+abbreviation Union :: "'a set set \<Rightarrow> 'a set"  ("\<Union>")
   where "\<Union>S \<equiv> \<Squnion>S"
 
 lemma Union_eq: "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
@@ -968,7 +968,7 @@
 lemma Union_UNIV: "\<Union>UNIV = UNIV"
   by (fact Sup_UNIV) (* already simp *)
 
-lemma Union_insert: "\<Union>insert a B = a \<union> \<Union>B"
+lemma Union_insert: "\<Union>(insert a B) = a \<union> \<Union>B"
   by (fact Sup_insert) (* already simp *)
 
 lemma Union_Un_distrib [simp]: "\<Union>(A \<union> B) = \<Union>A \<union> \<Union>B"
@@ -1017,7 +1017,7 @@
 
 translations
   "\<Union>x y. f"   \<rightleftharpoons> "\<Union>x. \<Union>y. f"
-  "\<Union>x. f"     \<rightleftharpoons> "\<Union>CONST range (\<lambda>x. f)"
+  "\<Union>x. f"     \<rightleftharpoons> "\<Union>(CONST range (\<lambda>x. f))"
   "\<Union>x\<in>A. f"   \<rightleftharpoons> "CONST Union ((\<lambda>x. f) ` A)"
 
 text \<open>
@@ -1268,7 +1268,7 @@
 proof -
   from assms have "inj_on f A"
     by (rule bij_betw_imp_inj_on)
-  then have "inj_on f (\<Union>Pow A)"
+  then have "inj_on f (\<Union>(Pow A))"
     by simp
   then have "inj_on (image f) (Pow A)"
     by (rule inj_on_image)
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Library/Disjoint_Sets.thy
--- a/src/HOL/Library/Disjoint_Sets.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Library/Disjoint_Sets.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -169,7 +169,7 @@
 qed
 
 lemma disjoint_UN:
-  assumes F: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)" and *: "disjoint_family_on (\<lambda>i. \<Union>F i) I"
+  assumes F: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)" and *: "disjoint_family_on (\<lambda>i. \<Union>(F i)) I"
   shows "disjoint (\<Union>i\<in>I. F i)"
 proof (safe intro!: disjointI del: equalityI)
   fix A B i j assume "A \<noteq> B" "A \<in> F i" "i \<in> I" "B \<in> F j" "j \<in> I"
@@ -179,7 +179,7 @@
       by (auto dest: disjointD)
   next
     assume "i \<noteq> j"
-    with * \<open>i\<in>I\<close> \<open>j\<in>I\<close> have "(\<Union>F i) \<inter> (\<Union>F j) = {}"
+    with * \<open>i\<in>I\<close> \<open>j\<in>I\<close> have "(\<Union>(F i)) \<inter> (\<Union>(F j)) = {}"
       by (rule disjoint_family_onD)
     with \<open>A\<in>F i\<close> \<open>i\<in>I\<close> \<open>B\<in>F j\<close> \<open>j\<in>I\<close>
     show "A \<inter> B = {}"
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Main.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -60,8 +60,8 @@
   top ("\<top>") and
   inf (infixl "\<sqinter>" 70) and
   sup (infixl "\<squnion>" 65) and
-  Inf ("\<Sqinter> _" [900] 900) and
-  Sup ("\<Squnion> _" [900] 900) and
+  Inf ("\<Sqinter>") and
+  Sup ("\<Squnion>") and
   ordLeq2 (infix "<=o" 50) and
   ordLeq3 (infix "\<le>o" 50) and
   ordLess2 (infix "<o" 50) and
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Partial_Function.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -32,15 +32,15 @@
     show ?thesis
     proof(cases "x \<le> \<Squnion>A")
       case True
-      have "\<Squnion>insert x A \<le> \<Squnion>A" using chain
+      have "\<Squnion>(insert x A) \<le> \<Squnion>A" using chain
         by(rule ccpo_Sup_least)(auto simp add: True intro: ccpo_Sup_upper[OF chain'])
-      hence "\<Squnion>insert x A = \<Squnion>A"
+      hence "\<Squnion>(insert x A) = \<Squnion>A"
         by(rule antisym)(blast intro: ccpo_Sup_upper[OF chain] ccpo_Sup_least[OF chain'])
       with \<open>\<Squnion>A \<in> A\<close> show ?thesis by simp
     next
       case False
       with chainD[OF chain, of x "\<Squnion>A"] \<open>\<Squnion>A \<in> A\<close>
-      have "\<Squnion>insert x A = x"
+      have "\<Squnion>(insert x A) = x"
         by(auto intro: antisym ccpo_Sup_least[OF chain] order_trans[OF ccpo_Sup_upper[OF chain']] ccpo_Sup_upper[OF chain])
       thus ?thesis by simp
     qed
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/UNITY/Transformers.thy
--- a/src/HOL/UNITY/Transformers.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/UNITY/Transformers.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -383,7 +383,7 @@
 by (simp add: wens_single_finite_Suc [symmetric]) 
 
 lemma wens_single_eq_Union:
-      "wens_single act B = \<Union>range (wens_single_finite act B)" 
+      "wens_single act B = \<Union>(range (wens_single_finite act B))" 
 by (simp add: wens_single_finite_def wens_single_def, blast) 
 
 lemma wens_single_finite_eq_Union:
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/ex/Adhoc_Overloading_Examples.thy
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -26,7 +26,7 @@
 text \<open>The set of variables of a term might be computed as follows.\<close>
 fun term_vars :: "('a, 'b) term \<Rightarrow> 'b set" where
   "term_vars (Var x) = {x}" |
-  "term_vars (Fun f ts) = \<Union>set (map term_vars ts)"
+  "term_vars (Fun f ts) = \<Union>(set (map term_vars ts))"
 
 text \<open>However, also for \emph{rules} (i.e., pairs of terms) and term
 rewrite systems (i.e., sets of rules), the set of variables makes
diff -r bb0a354f6b46 -r aec42cee2521 src/HOL/ex/Perm_Fragments.thy
--- a/src/HOL/ex/Perm_Fragments.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/ex/Perm_Fragments.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -221,7 +221,7 @@
 qed
 
 lemma Union_orbits [simp]:
-  "\<Union>orbits f = affected f"
+  "\<Union>(orbits f) = affected f"
   by (auto simp add: orbits.simps intro: in_orbitsI in_orbit_affected)
 
 lemma finite_orbits [simp]: