# HG changeset patch
# User wenzelm
# Date 1435306833 -7200
# Node ID 48fdff264eb2be9c29d8914e2f34cb5a456340e4
# Parent  a645a0e6d790379ab78aead96fbd13d1885c619a
tuned whitespace;

diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -589,7 +589,7 @@
 lemma (in weak_upper_semilattice) finite_sup_insertI:
   assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
-  shows "P (\<Squnion> (insert x A))"
+  shows "P (\<Squnion>(insert x A))"
 proof (cases "A = {}")
   case True with P and xA show ?thesis
     by (simp add: finite_sup_least)
@@ -828,7 +828,7 @@
 lemma (in weak_lower_semilattice) finite_inf_insertI:
   assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
-  shows "P (\<Sqinter> (insert x A))"
+  shows "P (\<Sqinter>(insert x A))"
 proof (cases "A = {}")
   case True with P and xA show ?thesis
     by (simp add: finite_inf_greatest)
@@ -856,7 +856,7 @@
 
 lemma (in weak_lower_semilattice) inf_of_two_greatest:
   "[| x \<in> carrier L; y \<in> carrier L |] ==>
-  greatest L (\<Sqinter> {x, y}) (Lower L {x, y})"
+  greatest L (\<Sqinter>{x, y}) (Lower L {x, y})"
 proof (unfold inf_def)
   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast
@@ -904,8 +904,8 @@
 proof -
   (* FIXME: improved simp, see weak_join_assoc above *)
   have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
-  also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma)
-  also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
+  also from L have "... .= \<Sqinter>{z, x, y}" by (simp add: weak_meet_assoc_lemma)
+  also from L have "... = \<Sqinter>{x, y, z}" by (simp add: insert_commute)
   also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric])
   finally show ?thesis by (simp add: L)
 qed
@@ -1286,15 +1286,15 @@
 next
   fix B
   assume "B \<subseteq> carrier ?L"
-  then have "least ?L (\<Union> B) (Upper ?L B)"
+  then have "least ?L (\<Union>B) (Upper ?L B)"
     by (fastforce intro!: least_UpperI simp: Upper_def)
   then show "EX s. least ?L s (Upper ?L B)" ..
 next
   fix B
   assume "B \<subseteq> carrier ?L"
-  then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
-    txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
-      @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
+  then have "greatest ?L (\<Inter>B \<inter> A) (Lower ?L B)"
+    txt {* @{term "\<Inter>B"} is not the infimum of @{term B}:
+      @{term "\<Inter>{} = UNIV"} which is in general bigger than @{term "A"}! *}
     by (fastforce intro!: greatest_LowerI simp: Lower_def)
   then show "EX i. greatest ?L i (Lower ?L B)" ..
 qed
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/BNF_Cardinal_Order_Relation.thy
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -1051,10 +1051,10 @@
 lemma card_of_UNION_ordLeq_infinite:
 assumes INF: "\<not>finite B" and
         LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
-shows "|\<Union> i \<in> I. A i| \<le>o |B|"
+shows "|\<Union>i \<in> I. A i| \<le>o |B|"
 proof(cases "I = {}", simp add: card_of_empty)
   assume *: "I \<noteq> {}"
-  have "|\<Union> i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
+  have "|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
   using card_of_UNION_Sigma by blast
   moreover have "|SIGMA i : I. A i| \<le>o |B|"
   using assms card_of_Sigma_ordLeq_infinite by blast
@@ -1064,14 +1064,14 @@
 corollary card_of_UNION_ordLeq_infinite_Field:
 assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
         LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
-shows "|\<Union> i \<in> I. A i| \<le>o r"
+shows "|\<Union>i \<in> I. A i| \<le>o r"
 proof-
   let ?B  = "Field r"
   have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso
   ordIso_symmetric by blast
   hence "|I| \<le>o |?B|"  "\<forall>i \<in> I. |A i| \<le>o |?B|"
   using LEQ_I LEQ ordLeq_ordIso_trans by blast+
-  hence  "|\<Union> i \<in> I. A i| \<le>o |?B|" using INF LEQ
+  hence  "|\<Union>i \<in> I. A i| \<le>o |?B|" using INF LEQ
   card_of_UNION_ordLeq_infinite by blast
   thus ?thesis using 1 ordLeq_ordIso_trans by blast
 qed
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/BNF_Wellorder_Embedding.thy
--- a/src/HOL/BNF_Wellorder_Embedding.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/BNF_Wellorder_Embedding.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -26,7 +26,7 @@
 assumes WELL: "Well_order r" and
         OF: "\<And> i. i \<in> I \<Longrightarrow> wo_rel.ofilter r (A i)" and
        INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
-shows "inj_on f (\<Union> i \<in> I. A i)"
+shows "inj_on f (\<Union>i \<in> I. A i)"
 proof-
   have "wo_rel r" using WELL by (simp add: wo_rel_def)
   hence "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i <= A j \<or> A j <= A i"
@@ -487,7 +487,7 @@
   have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
   have OF: "wo_rel.ofilter r (underS r a)"
   by (auto simp add: Well wo_rel.underS_ofilter)
-  hence UN: "underS r a = (\<Union>  b \<in> underS r a. under r b)"
+  hence UN: "underS r a = (\<Union>b \<in> underS r a. under r b)"
   using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast
   (* Gather facts about elements of underS r a *)
   {fix b assume *: "b \<in> underS r a"
@@ -520,13 +520,13 @@
   (*  *)
   have OF': "wo_rel.ofilter r' (f`(underS r a))"
   proof-
-    have "f`(underS r a) = f`(\<Union>  b \<in> underS r a. under r b)"
+    have "f`(underS r a) = f`(\<Union>b \<in> underS r a. under r b)"
     using UN by auto
-    also have "\<dots> = (\<Union>  b \<in> underS r a. f`(under r b))" by blast
-    also have "\<dots> = (\<Union>  b \<in> underS r a. (under r' (f b)))"
+    also have "\<dots> = (\<Union>b \<in> underS r a. f`(under r b))" by blast
+    also have "\<dots> = (\<Union>b \<in> underS r a. (under r' (f b)))"
     using bFact by auto
     finally
-    have "f`(underS r a) = (\<Union>  b \<in> underS r a. (under r' (f b)))" .
+    have "f`(underS r a) = (\<Union>b \<in> underS r a. (under r' (f b)))" .
     thus ?thesis
     using Well' bFact
           wo_rel.ofilter_UNION[of r' "underS r a" "\<lambda> b. under r' (f b)"] by fastforce
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/BNF_Wellorder_Relation.thy
--- a/src/HOL/BNF_Wellorder_Relation.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/BNF_Wellorder_Relation.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -478,20 +478,20 @@
 qed
 
 lemma ofilter_UNION:
-"(\<And> i. i \<in> I \<Longrightarrow> ofilter(A i)) \<Longrightarrow> ofilter (\<Union> i \<in> I. A i)"
+"(\<And> i. i \<in> I \<Longrightarrow> ofilter(A i)) \<Longrightarrow> ofilter (\<Union>i \<in> I. A i)"
 unfolding ofilter_def by blast
 
 lemma ofilter_under_UNION:
 assumes "ofilter A"
-shows "A = (\<Union> a \<in> A. under a)"
+shows "A = (\<Union>a \<in> A. under a)"
 proof
   have "\<forall>a \<in> A. under a \<le> A"
   using assms ofilter_def by auto
-  thus "(\<Union> a \<in> A. under a) \<le> A" by blast
+  thus "(\<Union>a \<in> A. under a) \<le> A" by blast
 next
   have "\<forall>a \<in> A. a \<in> under a"
   using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast
-  thus "A \<le> (\<Union> a \<in> A. under a)" by blast
+  thus "A \<le> (\<Union>a \<in> A. under a)" by blast
 qed
 
 subsubsection{* Other properties *}
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Cardinals/Cardinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -297,8 +297,8 @@
 assumes "|A| \<le>o k" and "\<forall> a \<in> A. |vimage f {a}| \<le>o k" and "Cinfinite k"
 shows "|vimage f A| \<le>o k"
 proof-
-  have "vimage f A = (\<Union> a \<in> A. vimage f {a})" by auto
-  also have "|\<Union> a \<in> A. vimage f {a}| \<le>o k"
+  have "vimage f A = (\<Union>a \<in> A. vimage f {a})" by auto
+  also have "|\<Union>a \<in> A. vimage f {a}| \<le>o k"
   using UNION_Cinfinite_bound[OF assms] .
   finally show ?thesis .
 qed
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -715,7 +715,7 @@
 lemma lists_def2: "lists A = {l. set l \<le> A}"
 using in_listsI by blast
 
-lemma lists_UNION_nlists: "lists A = (\<Union> n. nlists A n)"
+lemma lists_UNION_nlists: "lists A = (\<Union>n. nlists A n)"
 unfolding lists_def2 nlists_def by blast
 
 lemma card_of_lists: "|A| \<le>o |lists A|"
@@ -1455,7 +1455,7 @@
 unfolding Func_option_def Pfunc_def by auto
 
 lemma Pfunc_Func_option:
-"Pfunc A B = (\<Union> A' \<in> Pow A. Func_option A' B)"
+"Pfunc A B = (\<Union>A' \<in> Pow A. Func_option A' B)"
 proof safe
   fix f assume f: "f \<in> Pfunc A B"
   show "f \<in> (\<Union>A'\<in>Pow A. Func_option A' B)"
@@ -1504,7 +1504,7 @@
 assumes "B \<noteq> {}"
 shows "|Pfunc A B| \<le>o |Pow A <*> Func_option A B|"
 proof-
-  have "|Pfunc A B| =o |\<Union> A' \<in> Pow A. Func_option A' B|" (is "_ =o ?K")
+  have "|Pfunc A B| =o |\<Union>A' \<in> Pow A. Func_option A' B|" (is "_ =o ?K")
     unfolding Pfunc_Func_option by(rule card_of_refl)
   also have "?K \<le>o |Sigma (Pow A) (\<lambda> A'. Func_option A' B)|" using card_of_UNION_Sigma .
   also have "|Sigma (Pow A) (\<lambda> A'. Func_option A' B)| \<le>o |Pow A <*> Func_option A B|"
@@ -1635,14 +1635,14 @@
 qed
 
 lemma relChain_stabilize:
-assumes rc: "relChain r As" and AsB: "(\<Union> i \<in> Field r. As i) \<subseteq> B" and Br: "|B| <o r"
+assumes rc: "relChain r As" and AsB: "(\<Union>i \<in> Field r. As i) \<subseteq> B" and Br: "|B| <o r"
 and ir: "\<not>finite (Field r)" and cr: "Card_order r"
 shows "\<exists> i \<in> Field r. As (succ r i) = As i"
 proof(rule ccontr, auto)
   have 0: "wo_rel r" and 00: "Well_order r"
   unfolding wo_rel_def by (metis card_order_on_well_order_on cr)+
   have L: "isLimOrd r" using ir cr by (metis card_order_infinite_isLimOrd)
-  have AsBs: "(\<Union> i \<in> Field r. As (succ r i)) \<subseteq> B"
+  have AsBs: "(\<Union>i \<in> Field r. As (succ r i)) \<subseteq> B"
   using AsB L apply safe by (metis "0" UN_I set_mp wo_rel.isLimOrd_succ)
   assume As_s: "\<forall>i\<in>Field r. As (succ r i) \<noteq> As i"
   have 1: "\<forall>i j. (i,j) \<in> r \<and> i \<noteq> j \<longrightarrow> As i \<subset> As j"
@@ -1719,7 +1719,7 @@
    obtain j0 where j0: "j0 \<in> Field r" using Fi by auto
    def g \<equiv> "\<lambda> a. if F a \<noteq> {} then gg a else j0"
    have g: "\<forall> a \<in> A. \<forall> u \<in> F a. (f (a,u),g a) \<in> r" using gg unfolding g_def by auto
-   hence 1: "Field r \<subseteq> (\<Union> a \<in> A. under r (g a))"
+   hence 1: "Field r \<subseteq> (\<Union>a \<in> A. under r (g a))"
    using f[symmetric] unfolding under_def image_def by auto
    have gA: "g ` A \<subseteq> Field r" using gg j0 unfolding Field_def g_def by auto
    moreover have "cofinal (g ` A) r" unfolding cofinal_def proof safe
@@ -1751,10 +1751,10 @@
   {assume Kr: "|K| <o r"
    then obtain f where "\<forall> a \<in> Field r. f a \<in> K \<and> a \<noteq> f a \<and> (a, f a) \<in> r"
    using cof unfolding cofinal_def by metis
-   hence "Field r \<subseteq> (\<Union> a \<in> K. underS r a)" unfolding underS_def by auto
-   hence "r \<le>o |\<Union> a \<in> K. underS r a|" using cr
+   hence "Field r \<subseteq> (\<Union>a \<in> K. underS r a)" unfolding underS_def by auto
+   hence "r \<le>o |\<Union>a \<in> K. underS r a|" using cr
    by (metis Card_order_iff_ordLeq_card_of card_of_mono1 ordLeq_transitive)
-   also have "|\<Union> a \<in> K. underS r a| \<le>o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma)
+   also have "|\<Union>a \<in> K. underS r a| \<le>o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma)
    also
    {have "\<forall> a \<in> K. |underS r a| <o r" using K by (metis card_of_underS cr subsetD)
     hence "|SIGMA a: K. underS r a| <o r" using st Kr unfolding stable_def by auto
@@ -1818,9 +1818,9 @@
 lemma stable_UNION:
 assumes ST: "stable r" and A_LESS: "|A| <o r" and
         F_LESS: "\<And> a. a \<in> A \<Longrightarrow> |F a| <o r"
-shows "|\<Union> a \<in> A. F a| <o r"
+shows "|\<Union>a \<in> A. F a| <o r"
 proof-
-  have "|\<Union> a \<in> A. F a| \<le>o |SIGMA a : A. F a|"
+  have "|\<Union>a \<in> A. F a| \<le>o |SIGMA a : A. F a|"
   using card_of_UNION_Sigma by blast
   thus ?thesis using assms stable_elim ordLeq_ordLess_trans by blast
 qed
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Cardinals/Order_Relation_More.thy
--- a/src/HOL/Cardinals/Order_Relation_More.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Cardinals/Order_Relation_More.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -133,12 +133,12 @@
 
 lemma Refl_under_Under:
 assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "Under r A = (\<Inter> a \<in> A. under r a)"
+shows "Under r A = (\<Inter>a \<in> A. under r a)"
 proof
-  show "Under r A \<subseteq> (\<Inter> a \<in> A. under r a)"
+  show "Under r A \<subseteq> (\<Inter>a \<in> A. under r a)"
   by(unfold Under_def under_def, auto)
 next
-  show "(\<Inter> a \<in> A. under r a) \<subseteq> Under r A"
+  show "(\<Inter>a \<in> A. under r a) \<subseteq> Under r A"
   proof(auto)
     fix x
     assume *: "\<forall>xa \<in> A. x \<in> under r xa"
@@ -157,12 +157,12 @@
 
 lemma Refl_underS_UnderS:
 assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "UnderS r A = (\<Inter> a \<in> A. underS r a)"
+shows "UnderS r A = (\<Inter>a \<in> A. underS r a)"
 proof
-  show "UnderS r A \<subseteq> (\<Inter> a \<in> A. underS r a)"
+  show "UnderS r A \<subseteq> (\<Inter>a \<in> A. underS r a)"
   by(unfold UnderS_def underS_def, auto)
 next
-  show "(\<Inter> a \<in> A. underS r a) \<subseteq> UnderS r A"
+  show "(\<Inter>a \<in> A. underS r a) \<subseteq> UnderS r A"
   proof(auto)
     fix x
     assume *: "\<forall>xa \<in> A. x \<in> underS r xa"
@@ -181,12 +181,12 @@
 
 lemma Refl_above_Above:
 assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "Above r A = (\<Inter> a \<in> A. above r a)"
+shows "Above r A = (\<Inter>a \<in> A. above r a)"
 proof
-  show "Above r A \<subseteq> (\<Inter> a \<in> A. above r a)"
+  show "Above r A \<subseteq> (\<Inter>a \<in> A. above r a)"
   by(unfold Above_def above_def, auto)
 next
-  show "(\<Inter> a \<in> A. above r a) \<subseteq> Above r A"
+  show "(\<Inter>a \<in> A. above r a) \<subseteq> Above r A"
   proof(auto)
     fix x
     assume *: "\<forall>xa \<in> A. x \<in> above r xa"
@@ -205,12 +205,12 @@
 
 lemma Refl_aboveS_AboveS:
 assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "AboveS r A = (\<Inter> a \<in> A. aboveS r a)"
+shows "AboveS r A = (\<Inter>a \<in> A. aboveS r a)"
 proof
-  show "AboveS r A \<subseteq> (\<Inter> a \<in> A. aboveS r a)"
+  show "AboveS r A \<subseteq> (\<Inter>a \<in> A. aboveS r a)"
   by(unfold AboveS_def aboveS_def, auto)
 next
-  show "(\<Inter> a \<in> A. aboveS r a) \<subseteq> AboveS r A"
+  show "(\<Inter>a \<in> A. aboveS r a) \<subseteq> AboveS r A"
   proof(auto)
     fix x
     assume *: "\<forall>xa \<in> A. x \<in> aboveS r xa"
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Cardinals/Wellorder_Embedding.thy
--- a/src/HOL/Cardinals/Wellorder_Embedding.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Cardinals/Wellorder_Embedding.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -17,7 +17,7 @@
 assumes WELL: "Well_order r" and
         OF: "\<And> i. i \<in> I \<Longrightarrow> ofilter r (A i)" and
        BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
-shows "bij_betw f (\<Union> i \<in> I. A i) (\<Union> i \<in> I. A' i)"
+shows "bij_betw f (\<Union>i \<in> I. A i) (\<Union>i \<in> I. A' i)"
 proof-
   have "wo_rel r" using WELL by (simp add: wo_rel_def)
   hence "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i"
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Cardinals/Wellorder_Relation.thy
--- a/src/HOL/Cardinals/Wellorder_Relation.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -437,7 +437,7 @@
 unfolding ofilter_def by blast
 
 lemma ofilter_INTER:
-"\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter> i \<in> I. A i)"
+"\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter>i \<in> I. A i)"
 unfolding ofilter_def by blast
 
 lemma ofilter_Inter:
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Complete_Lattices.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -1204,7 +1204,7 @@
   "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
   by (fact Sup_image_eq)
 
-lemma Union_SetCompr_eq: "\<Union> {f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}"
+lemma Union_SetCompr_eq: "\<Union>{f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}"
   by blast
 
 lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<exists>x\<in>A. b \<in> B x)"
@@ -1360,7 +1360,7 @@
 lemma inj_on_UNION_chain:
   assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
          INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
-  shows "inj_on f (\<Union> i \<in> I. A i)"
+  shows "inj_on f (\<Union>i \<in> I. A i)"
 proof -
   {
     fix i j x y
@@ -1390,11 +1390,11 @@
 lemma bij_betw_UNION_chain:
   assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
          BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
-  shows "bij_betw f (\<Union> i \<in> I. A i) (\<Union> i \<in> I. A' i)"
+  shows "bij_betw f (\<Union>i \<in> I. A i) (\<Union>i \<in> I. A' i)"
 proof (unfold bij_betw_def, auto)
   have "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
   using BIJ bij_betw_def[of f] by auto
-  thus "inj_on f (\<Union> i \<in> I. A i)"
+  thus "inj_on f (\<Union>i \<in> I. A i)"
   using CH inj_on_UNION_chain[of I A f] by auto
 next
   fix i x
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy
--- a/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -257,7 +257,7 @@
 qed
 
 corollary Fr_subtr:
-"Fr ns tr = \<Union> {Fr ns tr' | tr'. subtr ns tr' tr}"
+"Fr ns tr = \<Union>{Fr ns tr' | tr'. subtr ns tr' tr}"
 unfolding Fr_def proof safe
   fix t assume t: "inFr ns tr t"  hence "root tr \<in> ns" by (rule inFr_root_in)
   thus "t \<in> \<Union>{{t. inFr ns tr' t} |tr'. subtr ns tr' tr}"
@@ -272,7 +272,7 @@
   by (metis (lifting) subtr.Step)
 
 corollary Fr_subtr_cont:
-"Fr ns tr = \<Union> {Inl -` cont tr' | tr'. subtr ns tr' tr}"
+"Fr ns tr = \<Union>{Inl -` cont tr' | tr'. subtr ns tr' tr}"
 unfolding Fr_def
 apply safe
 apply (frule inFr_subtr)
@@ -290,7 +290,7 @@
 qed
 
 corollary Itr_subtr:
-"Itr ns tr = \<Union> {Itr ns tr' | tr'. subtr ns tr' tr}"
+"Itr ns tr = \<Union>{Itr ns tr' | tr'. subtr ns tr' tr}"
 unfolding Itr_def apply safe
 apply (metis (lifting, mono_tags) UnionI inItr_root_in mem_Collect_eq subtr.Refl)
 by (metis subtr_inItr)
@@ -1121,7 +1121,7 @@
 assumes r: "regular tr" and In: "root tr \<in> ns"
 shows "Fr ns tr =
        Inl -` (cont tr) \<union>
-       \<Union> {Fr (ns - {root tr}) tr' | tr'. Inr tr' \<in> cont tr}"
+       \<Union>{Fr (ns - {root tr}) tr' | tr'. Inr tr' \<in> cont tr}"
 unfolding Fr_def
 using In inFr.Base regular_inFr[OF assms] apply safe
 apply (simp, metis (full_types) mem_Collect_eq)
@@ -1161,7 +1161,7 @@
 lemma Lr_rec_in:
 assumes n: "n \<in> ns"
 shows "Lr ns n \<subseteq>
-{Inl -` tns \<union> (\<Union> {K n' | n'. Inr n' \<in> tns}) | tns K.
+{Inl -` tns \<union> (\<Union>{K n' | n'. Inr n' \<in> tns}) | tns K.
     (n,tns) \<in> P \<and>
     (\<forall> n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> Lr (ns - {n}) n')}"
 (is "Lr ns n \<subseteq> {?F tns K | tns K. (n,tns) \<in> P \<and> ?\<phi> tns K}")
@@ -1207,7 +1207,7 @@
 lemma L_rec_in:
 assumes n: "n \<in> ns"
 shows "
-{Inl -` tns \<union> (\<Union> {K n' | n'. Inr n' \<in> tns}) | tns K.
+{Inl -` tns \<union> (\<Union>{K n' | n'. Inr n' \<in> tns}) | tns K.
     (n,tns) \<in> P \<and>
     (\<forall> n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> L (ns - {n}) n')}
  \<subseteq> L ns n"
@@ -1247,7 +1247,7 @@
 function LL where
 "LL ns n =
  (if n \<notin> ns then {{}} else
- {Inl -` tns \<union> (\<Union> {K n' | n'. Inr n' \<in> tns}) | tns K.
+ {Inl -` tns \<union> (\<Union>{K n' | n'. Inr n' \<in> tns}) | tns K.
     (n,tns) \<in> P \<and>
     (\<forall> n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> LL (ns - {n}) n')})"
 by(pat_completeness, auto)
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Datatype_Examples/Lambda_Term.thy
--- a/src/HOL/Datatype_Examples/Lambda_Term.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Datatype_Examples/Lambda_Term.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -27,14 +27,14 @@
   "varsOf (Var a) = {a}"
 | "varsOf (App f x) = varsOf f \<union> varsOf x"
 | "varsOf (Lam x b) = {x} \<union> varsOf b"
-| "varsOf (Lt F t) = varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| fimage (map_prod id varsOf) F})"
+| "varsOf (Lt F t) = varsOf t \<union> (\<Union>{{x} \<union> X | x X. (x,X) |\<in>| fimage (map_prod id varsOf) F})"
 
 primrec fvarsOf :: "'a trm \<Rightarrow> 'a set" where
   "fvarsOf (Var x) = {x}"
 | "fvarsOf (App t1 t2) = fvarsOf t1 \<union> fvarsOf t2"
 | "fvarsOf (Lam x t) = fvarsOf t - {x}"
 | "fvarsOf (Lt xts t) = fvarsOf t - {x | x X. (x,X) |\<in>| fimage (map_prod id varsOf) xts} \<union>
-    (\<Union> {X | x X. (x,X) |\<in>| fimage (map_prod id varsOf) xts})"
+    (\<Union>{X | x X. (x,X) |\<in>| fimage (map_prod id varsOf) xts})"
 
 lemma diff_Un_incl_triv: "\<lbrakk>A \<subseteq> D; C \<subseteq> E\<rbrakk> \<Longrightarrow> A - B \<union> C \<subseteq> D \<union> E" by blast
 
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -1433,7 +1433,7 @@
 
 lemma insert_partition:
   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
-  \<Longrightarrow> x \<inter> \<Union> F = {}"
+  \<Longrightarrow> x \<inter> \<Union>F = {}"
 by auto
 
 lemma finite_psubset_induct[consumes 1, case_names psubset]:
@@ -1486,13 +1486,13 @@
 text{* main cardinality theorem *}
 lemma card_partition [rule_format]:
   "finite C ==>
-     finite (\<Union> C) -->
+     finite (\<Union>C) -->
      (\<forall>c\<in>C. card c = k) -->
      (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
-     k * card(C) = card (\<Union> C)"
+     k * card(C) = card (\<Union>C)"
 apply (erule finite_induct, simp)
 apply (simp add: card_Un_disjoint insert_partition 
-       finite_subset [of _ "\<Union> (insert x F)"])
+       finite_subset [of _ "\<Union>(insert x F)"])
 done
 
 lemma card_eq_UNIV_imp_eq_UNIV:
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/HOLCF/Cont.thy
--- a/src/HOL/HOLCF/Cont.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/HOLCF/Cont.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -91,7 +91,7 @@
 text {* continuity implies preservation of lubs *}
 
 lemma cont2contlubE:
-  "\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion> i. Y i) = (\<Squnion> i. f (Y i))"
+  "\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))"
 apply (rule lub_eqI [symmetric])
 apply (erule (1) contE)
 done
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -408,20 +408,20 @@
 qed
 
 lemma Ex_inj_on_UNION_Sigma:
-  "\<exists>f. (inj_on f (\<Union> i \<in> I. A i) \<and> f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i))"
+  "\<exists>f. (inj_on f (\<Union>i \<in> I. A i) \<and> f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i))"
 proof
   let ?phi = "\<lambda> a i. i \<in> I \<and> a \<in> A i"
   let ?sm = "\<lambda> a. SOME i. ?phi a i"
   let ?f = "\<lambda>a. (?sm a, a)"
-  have "inj_on ?f (\<Union> i \<in> I. A i)" unfolding inj_on_def by auto
+  have "inj_on ?f (\<Union>i \<in> I. A i)" unfolding inj_on_def by auto
   moreover
   { { fix i a assume "i \<in> I" and "a \<in> A i"
       hence "?sm a \<in> I \<and> a \<in> A(?sm a)" using someI[of "?phi a" i] by auto
     }
-    hence "?f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i)" by auto
+    hence "?f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i)" by auto
   }
   ultimately
-  show "inj_on ?f (\<Union> i \<in> I. A i) \<and> ?f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i)"
+  show "inj_on ?f (\<Union>i \<in> I. A i) \<and> ?f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i)"
   by auto
 qed
 
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Hoare/SchorrWaite.thy
--- a/src/HOL/Hoare/SchorrWaite.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Hoare/SchorrWaite.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -17,7 +17,7 @@
 
 definition
   relS :: "('a \<Rightarrow> 'a ref) set \<Rightarrow> ('a \<times> 'a) set"
-  where "relS M = (\<Union> m \<in> M. rel m)"
+  where "relS M = (\<Union>m \<in> M. rel m)"
 
 definition
   addrs :: "'a ref set \<Rightarrow> 'a set"
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Library/Indicator_Function.thy
--- a/src/HOL/Library/Indicator_Function.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Library/Indicator_Function.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -87,18 +87,18 @@
     by auto
   then have 
     "\<And>n. (indicator (A (n + i)) x :: 'a) = 1"
-    "(indicator (\<Union> i. A i) x :: 'a) = 1"
+    "(indicator (\<Union>i. A i) x :: 'a) = 1"
     using incseqD[OF \<open>incseq A\<close>, of i "n + i" for n] \<open>x \<in> A i\<close> by (auto simp: indicator_def)
   then show ?thesis
     by (rule_tac LIMSEQ_offset[of _ i]) simp
 qed (auto simp: indicator_def)
 
 lemma LIMSEQ_indicator_UN:
-  "(\<lambda>k. indicator (\<Union> i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
+  "(\<lambda>k. indicator (\<Union>i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
 proof -
-  have "(\<lambda>k. indicator (\<Union> i<k. A i) x::'a) ----> indicator (\<Union>k. \<Union> i<k. A i) x"
+  have "(\<lambda>k. indicator (\<Union>i<k. A i) x::'a) ----> indicator (\<Union>k. \<Union>i<k. A i) x"
     by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans)
-  also have "(\<Union>k. \<Union> i<k. A i) = (\<Union>i. A i)"
+  also have "(\<Union>k. \<Union>i<k. A i) = (\<Union>i. A i)"
     by auto
   finally show ?thesis .
 qed
@@ -123,7 +123,7 @@
 proof -
   have "(\<lambda>k. indicator (\<Inter>i<k. A i) x::'a) ----> indicator (\<Inter>k. \<Inter>i<k. A i) x"
     by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans)
-  also have "(\<Inter>k. \<Inter> i<k. A i) = (\<Inter>i. A i)"
+  also have "(\<Inter>k. \<Inter>i<k. A i) = (\<Inter>i. A i)"
     by auto
   finally show ?thesis .
 qed
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -604,7 +604,7 @@
 lemma analytic_on_Un: "f analytic_on (s \<union> t) \<longleftrightarrow> f analytic_on s \<and> f analytic_on t"
   by (auto simp: analytic_on_def)
 
-lemma analytic_on_Union: "f analytic_on (\<Union> s) \<longleftrightarrow> (\<forall>t \<in> s. f analytic_on t)"
+lemma analytic_on_Union: "f analytic_on (\<Union>s) \<longleftrightarrow> (\<forall>t \<in> s. f analytic_on t)"
   by (auto simp: analytic_on_def)
 
 lemma analytic_on_UN: "f analytic_on (\<Union>i\<in>I. s i) \<longleftrightarrow> (\<forall>i\<in>I. f analytic_on (s i))"
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -384,7 +384,7 @@
 lemma affine_UNIV[intro]: "affine UNIV"
   unfolding affine_def by auto
 
-lemma affine_Inter[intro]: "(\<forall>s\<in>f. affine s) \<Longrightarrow> affine (\<Inter> f)"
+lemma affine_Inter[intro]: "(\<forall>s\<in>f. affine s) \<Longrightarrow> affine (\<Inter>f)"
   unfolding affine_def by auto
 
 lemma affine_Int[intro]: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)"
@@ -4552,7 +4552,7 @@
   shows "\<exists>a. a \<noteq> 0 \<and> (\<forall>x\<in>s. 0 \<le> inner a x)"
 proof -
   let ?k = "\<lambda>c. {x::'a. 0 \<le> inner c x}"
-  have "frontier (cball 0 1) \<inter> (\<Inter> (?k ` s)) \<noteq> {}"
+  have "frontier (cball 0 1) \<inter> (\<Inter>(?k ` s)) \<noteq> {}"
     apply (rule compact_imp_fip)
     apply (rule compact_frontier[OF compact_cball])
     defer
@@ -4758,7 +4758,7 @@
 lemma convex_halfspace_intersection:
   fixes s :: "('a::euclidean_space) set"
   assumes "closed s" "convex s"
-  shows "s = \<Inter> {h. s \<subseteq> h \<and> (\<exists>a b. h = {x. inner a x \<le> b})}"
+  shows "s = \<Inter>{h. s \<subseteq> h \<and> (\<exists>a b. h = {x. inner a x \<le> b})}"
   apply (rule set_eqI)
   apply rule
   unfolding Inter_iff Ball_def mem_Collect_eq
@@ -4935,7 +4935,7 @@
   fixes f :: "'a::euclidean_space set set"
   assumes "card f = n"
     and "n \<ge> DIM('a) + 1"
-    and "\<forall>s\<in>f. convex s" "\<forall>t\<subseteq>f. card t = DIM('a) + 1 \<longrightarrow> \<Inter> t \<noteq> {}"
+    and "\<forall>s\<in>f. convex s" "\<forall>t\<subseteq>f. card t = DIM('a) + 1 \<longrightarrow> \<Inter>t \<noteq> {}"
   shows "\<Inter>f \<noteq> {}"
   using assms
 proof (induct n arbitrary: f)
@@ -5033,7 +5033,7 @@
 lemma helly:
   fixes f :: "'a::euclidean_space set set"
   assumes "card f \<ge> DIM('a) + 1" "\<forall>s\<in>f. convex s"
-    and "\<forall>t\<subseteq>f. card t = DIM('a) + 1 \<longrightarrow> \<Inter> t \<noteq> {}"
+    and "\<forall>t\<subseteq>f. card t = DIM('a) + 1 \<longrightarrow> \<Inter>t \<noteq> {}"
   shows "\<Inter>f \<noteq> {}"
   apply (rule helly_induct)
   using assms
@@ -7756,7 +7756,7 @@
   have "\<Inter>{closure S |S. S \<in> I} \<le> closure (\<Inter>{rel_interior S |S. S \<in> I})"
     using convex_closure_rel_interior_inter assms by auto
   moreover
-  have "closure (\<Inter>{rel_interior S |S. S \<in> I}) \<le> closure (\<Inter> I)"
+  have "closure (\<Inter>{rel_interior S |S. S \<in> I}) \<le> closure (\<Inter>I)"
     using rel_interior_inter_aux closure_mono[of "\<Inter>{rel_interior S |S. S \<in> I}" "\<Inter>I"]
     by auto
   ultimately show ?thesis
@@ -8750,7 +8750,7 @@
     done
   ultimately have "convex hull (\<Union>(K ` I)) \<supseteq> K0"
     unfolding K0_def
-    using hull_minimal[of _ "convex hull (\<Union> (K ` I))" "cone"]
+    using hull_minimal[of _ "convex hull (\<Union>(K ` I))" "cone"]
     by blast
   then have "K0 = convex hull (\<Union>(K ` I))"
     using geq by auto
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -648,7 +648,7 @@
 lemma gauge_inters:
   assumes "finite s"
     and "\<forall>d\<in>s. gauge (f d)"
-  shows "gauge (\<lambda>x. \<Inter> {f d x | d. d \<in> s})"
+  shows "gauge (\<lambda>x. \<Inter>{f d x | d. d \<in> s})"
 proof -
   have *: "\<And>x. {f d x |d. d \<in> s} = (\<lambda>d. f d x) ` s"
     by auto
@@ -871,7 +871,7 @@
   assumes "finite f"
     and "f \<noteq> {}"
     and "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::euclidean_space) set)"
-  shows "\<exists>p. p division_of (\<Inter> f)"
+  shows "\<exists>p. p division_of (\<Inter>f)"
   using assms
 proof (induct f rule: finite_induct)
   case (insert x f)
@@ -1066,7 +1066,7 @@
       done }
   then have "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
     by (meson Diff_subset division_of_subset)
-  then have "\<exists>d. d division_of \<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)"
+  then have "\<exists>d. d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)"
     apply -
     apply (rule elementary_inters [OF finite_imageI[OF p(1)]])
     apply (auto simp: False elementary_inters [OF finite_imageI[OF p(1)]])
@@ -1669,7 +1669,7 @@
   unfolding fine_def by auto
 
 lemma fine_inters:
- "(\<lambda>x. \<Inter> {f d x | d.  d \<in> s}) fine p \<longleftrightarrow> (\<forall>d\<in>s. (f d) fine p)"
+ "(\<lambda>x. \<Inter>{f d x | d.  d \<in> s}) fine p \<longleftrightarrow> (\<forall>d\<in>s. (f d) fine p)"
   unfolding fine_def by blast
 
 lemma fine_union: "d fine p1 \<Longrightarrow> d fine p2 \<Longrightarrow> d fine (p1 \<union> p2)"
@@ -1851,7 +1851,7 @@
       by (blast intro: that)
   }
   assume as: "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d)"
-  have "P (\<Union> ?A)"
+  have "P (\<Union>?A)"
   proof (rule UN_cases)
     let ?B = "(\<lambda>s. cbox (\<Sum>i\<in>Basis. (if i \<in> s then a\<bullet>i else (a\<bullet>i + b\<bullet>i) / 2) *\<^sub>R i::'a)
       (\<Sum>i\<in>Basis. (if i \<in> s then (a\<bullet>i + b\<bullet>i) / 2 else b\<bullet>i) *\<^sub>R i)) ` {s. s \<subseteq> Basis}"
@@ -1926,7 +1926,7 @@
       qed
     qed
   qed
-  also have "\<Union> ?A = cbox a b"
+  also have "\<Union>?A = cbox a b"
   proof (rule set_eqI,rule)
     fix x
     assume "x \<in> \<Union>?A"
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -413,7 +413,7 @@
 subsection \<open>General notion of a topology as a value\<close>
 
 definition "istopology L \<longleftrightarrow>
-  L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
+  L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union>K))"
 
 typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
   morphisms "openin" "topology"
@@ -462,7 +462,7 @@
 lemma openin_Int[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<inter> T)"
   using openin_clauses by simp
 
-lemma openin_Union[intro]: "(\<forall>S \<in>K. openin U S) \<Longrightarrow> openin U (\<Union> K)"
+lemma openin_Union[intro]: "(\<forall>S \<in>K. openin U S) \<Longrightarrow> openin U (\<Union>K)"
   using openin_clauses by simp
 
 lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)"
@@ -501,13 +501,13 @@
 lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)"
   by (auto simp add: Diff_Un closedin_def)
 
-lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union> {A - s|s. s\<in>S}"
+lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union>{A - s|s. s\<in>S}"
   by auto
 
 lemma closedin_Inter[intro]:
   assumes Ke: "K \<noteq> {}"
     and Kc: "\<forall>S \<in>K. closedin U S"
-  shows "closedin U (\<Inter> K)"
+  shows "closedin U (\<Inter>K)"
   using Ke Kc unfolding closedin_def Diff_Inter by auto
 
 lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)"
@@ -575,7 +575,7 @@
       by blast
     have "\<Union>K = (\<Union>Sk) \<inter> V"
       using Sk by auto
-    moreover have "openin U (\<Union> Sk)"
+    moreover have "openin U (\<Union>Sk)"
       using Sk by (auto simp add: subset_eq)
     ultimately have "?L (\<Union>K)" by blast
   }
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Nominal/Examples/Class2.thy
--- a/src/HOL/Nominal/Examples/Class2.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Nominal/Examples/Class2.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -2888,8 +2888,8 @@
   and   X::"('a::pt_name) set set"
   and   pi2::"coname prm"
   and   Y::"('b::pt_coname) set set"
-  shows "(pi1\<bullet>(\<Inter> X)) = \<Inter> (pi1\<bullet>X)"
-  and   "(pi2\<bullet>(\<Inter> Y)) = \<Inter> (pi2\<bullet>Y)"
+  shows "(pi1\<bullet>(\<Inter>X)) = \<Inter>(pi1\<bullet>X)"
+  and   "(pi2\<bullet>(\<Inter>Y)) = \<Inter>(pi2\<bullet>Y)"
 apply(auto simp add: perm_set_def)
 apply(rule_tac x="(rev pi1)\<bullet>x" in exI)
 apply(perm_simp)
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -1888,9 +1888,9 @@
   assumes  pt: "pt TYPE('a) TYPE('x)"
   and      at: "at TYPE ('x)"
   and      fs: "fs TYPE('a) TYPE('x)"
-  shows "((supp x)::'x set) = (\<Inter> {S. finite S \<and> S supports x})"
+  shows "((supp x)::'x set) = (\<Inter>{S. finite S \<and> S supports x})"
 proof (rule equalityI)
-  show "((supp x)::'x set) \<subseteq> (\<Inter> {S. finite S \<and> S supports x})"
+  show "((supp x)::'x set) \<subseteq> (\<Inter>{S. finite S \<and> S supports x})"
   proof (clarify)
     fix S c
     assume b: "c\<in>((supp x)::'x set)" and "finite (S::'x set)" and "S supports x"
@@ -1898,7 +1898,7 @@
     with b show "c\<in>S" by force
   qed
 next
-  show "(\<Inter> {S. finite S \<and> S supports x}) \<subseteq> ((supp x)::'x set)"
+  show "(\<Inter>{S. finite S \<and> S supports x}) \<subseteq> ((supp x)::'x set)"
   proof (clarify, simp)
     fix c
     assume d: "\<forall>(S::'x set). finite S \<and> S supports x \<longrightarrow> c\<in>S"
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -83,7 +83,7 @@
         by (rule finite_subset) auto }
     
     { fix N i n x assume "i \<le> N" "n \<le> N" "x \<in> B i n"
-      then have 1: "\<exists>m\<le>N. x \<in> (\<Union> n\<le>N. B m n)" by auto
+      then have 1: "\<exists>m\<le>N. x \<in> (\<Union>n\<le>N. B m n)" by auto
       from m[OF this] obtain n where n: "m N x \<le> N" "n \<le> N" "x \<in> B (m N x) n" by auto
       moreover
       def L \<equiv> "LEAST n. x \<in> B (m N x) n"
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Probability/Caratheodory.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -804,7 +804,7 @@
     with Ca Cb have "Ca \<inter> Cb \<subseteq> {{}}" by auto
     then have C_Int_cases: "Ca \<inter> Cb = {{}} \<or> Ca \<inter> Cb = {}" by auto
 
-    from `a \<inter> b = {}` have "\<mu>' (\<Union> (Ca \<union> Cb)) = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c)"
+    from `a \<inter> b = {}` have "\<mu>' (\<Union>(Ca \<union> Cb)) = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c)"
       using Ca Cb by (intro \<mu>') (auto intro!: disjoint_union)
     also have "\<dots> = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c) + (\<Sum>c\<in>Ca \<inter> Cb. \<mu> c)"
       using C_Int_cases volume_empty[OF `volume M \<mu>`] by (elim disjE) simp_all
@@ -915,7 +915,7 @@
         then have "disjoint_family f"
           by (auto simp: disjoint_family_on_def f_def)
         moreover
-        have Ai_eq: "A i = (\<Union> x<card C. f x)"
+        have Ai_eq: "A i = (\<Union>x<card C. f x)"
           using f C Ai unfolding bij_betw_def by (simp add: Union_image_eq[symmetric])
         then have "\<Union>range f = A i"
           using f C Ai unfolding bij_betw_def by (auto simp: f_def)
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -172,17 +172,17 @@
   case empty thus ?case using f by (auto simp: positive_def)
 next
   case (insert x F)
-  hence in_M: "A x \<in> M" "(\<Union> i\<in>F. A i) \<in> M" "(\<Union> i\<in>F. A i) - A x \<in> M" using A by force+
-  have subs: "(\<Union> i\<in>F. A i) - A x \<subseteq> (\<Union> i\<in>F. A i)" by auto
-  have "(\<Union> i\<in>(insert x F). A i) = A x \<union> ((\<Union> i\<in>F. A i) - A x)" by auto
-  hence "f (\<Union> i\<in>(insert x F). A i) = f (A x \<union> ((\<Union> i\<in>F. A i) - A x))"
+  hence in_M: "A x \<in> M" "(\<Union>i\<in>F. A i) \<in> M" "(\<Union>i\<in>F. A i) - A x \<in> M" using A by force+
+  have subs: "(\<Union>i\<in>F. A i) - A x \<subseteq> (\<Union>i\<in>F. A i)" by auto
+  have "(\<Union>i\<in>(insert x F). A i) = A x \<union> ((\<Union>i\<in>F. A i) - A x)" by auto
+  hence "f (\<Union>i\<in>(insert x F). A i) = f (A x \<union> ((\<Union>i\<in>F. A i) - A x))"
     by simp
-  also have "\<dots> = f (A x) + f ((\<Union> i\<in>F. A i) - A x)"
+  also have "\<dots> = f (A x) + f ((\<Union>i\<in>F. A i) - A x)"
     using f(2) by (rule additiveD) (insert in_M, auto)
-  also have "\<dots> \<le> f (A x) + f (\<Union> i\<in>F. A i)"
+  also have "\<dots> \<le> f (A x) + f (\<Union>i\<in>F. A i)"
     using additive_increasing[OF f] in_M subs by (auto simp: increasing_def intro: add_left_mono)
   also have "\<dots> \<le> f (A x) + (\<Sum>i\<in>F. f (A i))" using insert by (auto intro: add_left_mono)
-  finally show "f (\<Union> i\<in>(insert x F). A i) \<le> (\<Sum>i\<in>(insert x F). f (A i))" using insert by simp
+  finally show "f (\<Union>i\<in>(insert x F). A i) \<le> (\<Sum>i\<in>(insert x F). f (A i))" using insert by simp
 qed
 
 lemma (in ring_of_sets) countably_additive_additive:
@@ -292,7 +292,7 @@
   have *: "(\<Union>n. (\<Union>i<n. A i)) = (\<Union>i. A i)" by auto
   have "(\<lambda>n. f (\<Union>i<n. A i)) ----> f (\<Union>i. A i)"
   proof (unfold *[symmetric], intro cont[rule_format])
-    show "range (\<lambda>i. \<Union> i<i. A i) \<subseteq> M" "(\<Union>i. \<Union> i<i. A i) \<in> M"
+    show "range (\<lambda>i. \<Union>i<i. A i) \<subseteq> M" "(\<Union>i. \<Union>i<i. A i) \<in> M"
       using A * by auto
   qed (force intro!: incseq_SucI)
   moreover have "\<And>n. f (\<Union>i<n. A i) = (\<Sum>i<n. f (A i))"
@@ -657,10 +657,10 @@
 
 lemma emeasure_UN_eq_0:
   assumes "\<And>i::nat. emeasure M (N i) = 0" and "range N \<subseteq> sets M"
-  shows "emeasure M (\<Union> i. N i) = 0"
+  shows "emeasure M (\<Union>i. N i) = 0"
 proof -
-  have "0 \<le> emeasure M (\<Union> i. N i)" using assms by auto
-  moreover have "emeasure M (\<Union> i. N i) \<le> 0"
+  have "0 \<le> emeasure M (\<Union>i. N i)" using assms by auto
+  moreover have "emeasure M (\<Union>i. N i) \<le> 0"
     using emeasure_subadditive_countably[OF assms(2)] assms(1) by simp
   ultimately show ?thesis by simp
 qed
@@ -1173,9 +1173,9 @@
       from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto
       with F show ?thesis by fastforce
     qed
-    show "emeasure M (\<Union> i\<le>n. F i) \<noteq> \<infinity>" for n
+    show "emeasure M (\<Union>i\<le>n. F i) \<noteq> \<infinity>" for n
     proof -
-      have "emeasure M (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. emeasure M (F i))"
+      have "emeasure M (\<Union>i\<le>n. F i) \<le> (\<Sum>i\<le>n. emeasure M (F i))"
         using F by (auto intro!: emeasure_subadditive_finite)
       also have "\<dots> < \<infinity>"
         using F by (auto simp: setsum_Pinfty)
@@ -1579,12 +1579,12 @@
   assumes "range f \<subseteq> sets M" "range g \<subseteq> sets M"
   assumes "disjoint_family f" "disjoint_family g"
   assumes "\<And> n :: nat. measure M (f n) = measure M (g n)"
-  shows "measure M (\<Union> i. f i) = measure M (\<Union> i. g i)"
+  shows "measure M (\<Union>i. f i) = measure M (\<Union>i. g i)"
 using assms
 proof -
-  have a: "(\<lambda> i. measure M (f i)) sums (measure M (\<Union> i. f i))"
+  have a: "(\<lambda> i. measure M (f i)) sums (measure M (\<Union>i. f i))"
     by (rule finite_measure_UNION[OF assms(1,3)])
-  have b: "(\<lambda> i. measure M (g i)) sums (measure M (\<Union> i. g i))"
+  have b: "(\<lambda> i. measure M (g i)) sums (measure M (\<Union>i. g i))"
     by (rule finite_measure_UNION[OF assms(2,4)])
   show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp
 qed
@@ -1592,9 +1592,9 @@
 lemma (in finite_measure) measure_countably_zero:
   assumes "range c \<subseteq> sets M"
   assumes "\<And> i. measure M (c i) = 0"
-  shows "measure M (\<Union> i :: nat. c i) = 0"
+  shows "measure M (\<Union>i :: nat. c i) = 0"
 proof (rule antisym)
-  show "measure M (\<Union> i :: nat. c i) \<le> 0"
+  show "measure M (\<Union>i :: nat. c i) \<le> 0"
     using finite_measure_subadditive_countably[OF assms(1)] by (simp add: assms(2))
 qed (simp add: measure_nonneg)
 
@@ -1633,12 +1633,12 @@
   assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> sets M"
   assumes "finite s"
   assumes disjoint: "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}"
-  assumes upper: "space M \<subseteq> (\<Union> i \<in> s. f i)"
+  assumes upper: "space M \<subseteq> (\<Union>i \<in> s. f i)"
   shows "measure M e = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
 proof -
-  have e: "e = (\<Union> i \<in> s. e \<inter> f i)"
+  have e: "e = (\<Union>i \<in> s. e \<inter> f i)"
     using `e \<in> sets M` sets.sets_into_space upper by blast
-  hence "measure M e = measure M (\<Union> i \<in> s. e \<inter> f i)" by simp
+  hence "measure M e = measure M (\<Union>i \<in> s. e \<inter> f i)" by simp
   also have "\<dots> = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
   proof (rule finite_measure_finite_Union)
     show "finite s" by fact
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Probability/Projective_Limit.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -282,15 +282,15 @@
       have Y_notempty: "\<And>n. n \<ge> 1 \<Longrightarrow> (Y n) \<noteq> {}"
       proof -
         fix n::nat assume "n \<ge> 1" hence "Y n \<subseteq> Z n" by fact
-        have "Y n = (\<Inter> i\<in>{1..n}. emb I (J n) (emb (J n) (J i) (K i)))" using J J_mono
+        have "Y n = (\<Inter>i\<in>{1..n}. emb I (J n) (emb (J n) (J i) (K i)))" using J J_mono
           by (auto simp: Y_def Z'_def)
-        also have "\<dots> = prod_emb I (\<lambda>_. borel) (J n) (\<Inter> i\<in>{1..n}. emb (J n) (J i) (K i))"
+        also have "\<dots> = prod_emb I (\<lambda>_. borel) (J n) (\<Inter>i\<in>{1..n}. emb (J n) (J i) (K i))"
           using `n \<ge> 1`
           by (subst prod_emb_INT) auto
         finally
         have Y_emb:
           "Y n = prod_emb I (\<lambda>_. borel) (J n)
-            (\<Inter> i\<in>{1..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i))" .
+            (\<Inter>i\<in>{1..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i))" .
         hence "Y n \<in> ?G" using J J_mono K_sets `n \<ge> 1` by (intro generatorI[OF _ _ _ _ Y_emb]) auto
         hence "\<bar>\<mu>G (Y n)\<bar> \<noteq> \<infinity>" unfolding Y_emb using J J_mono K_sets `n \<ge> 1`
           by (subst mu_G_eq) (auto simp: limP_finite proj_sets mu_G_eq)
@@ -317,11 +317,11 @@
             (auto dest!: bspec[where x=n]
             simp: extensional_restrict emeasure_eq_measure prod_emb_iff simp del: limP_finite
             intro!: measure_Diff[symmetric] set_mp[OF K_B])
-        also have subs: "Z n - Y n \<subseteq> (\<Union> i\<in>{1..n}. (Z i - Z' i))" using Z' Z `n \<ge> 1`
+        also have subs: "Z n - Y n \<subseteq> (\<Union>i\<in>{1..n}. (Z i - Z' i))" using Z' Z `n \<ge> 1`
           unfolding Y_def by (force simp: decseq_def)
-        have "Z n - Y n \<in> ?G" "(\<Union> i\<in>{1..n}. (Z i - Z' i)) \<in> ?G"
+        have "Z n - Y n \<in> ?G" "(\<Union>i\<in>{1..n}. (Z i - Z' i)) \<in> ?G"
           using `Z' _ \<in> ?G` `Z _ \<in> ?G` `Y _ \<in> ?G` by auto
-        hence "\<mu>G (Z n - Y n) \<le> \<mu>G (\<Union> i\<in>{1..n}. (Z i - Z' i))"
+        hence "\<mu>G (Z n - Y n) \<le> \<mu>G (\<Union>i\<in>{1..n}. (Z i - Z' i))"
           using subs G.additive_increasing[OF positive_mu_G[OF `I \<noteq> {}`] additive_mu_G[OF `I \<noteq> {}`]]
           unfolding increasing_def by auto
         also have "\<dots> \<le> (\<Sum> i\<in>{1..n}. \<mu>G (Z i - Z' i))" using `Z _ \<in> ?G` `Z' _ \<in> ?G`
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -625,7 +625,7 @@
       next
         case (Suc n)
         with `?O n \<in> ?Q` `?O (Suc n) \<in> ?Q`
-            emeasure_Diff[OF _ _ _ O_mono, of N n] emeasure_nonneg[of N "(\<Union> x\<le>n. Q' x)"]
+            emeasure_Diff[OF _ _ _ O_mono, of N n] emeasure_nonneg[of N "(\<Union>x\<le>n. Q' x)"]
         show ?thesis
           by (auto simp: sets_eq ereal_minus_eq_PInfty_iff Q_def)
       qed }
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Probability/ex/Dining_Cryptographers.thy
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -289,12 +289,12 @@
   have [simp]: "length xs = n" using assms
     by (auto simp: dc_crypto inversion_def [abs_def])
 
-  have "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union> i < n. ?set i)"
+  have "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union>i < n. ?set i)"
     unfolding dc_crypto payer_def by auto
-  also have "\<dots> = (\<Union> ?sets)" by auto
-  finally have eq_Union: "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union> ?sets)" by simp
+  also have "\<dots> = (\<Union>?sets)" by auto
+  finally have eq_Union: "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union>?sets)" by simp
 
-  have card_double: "2 * card ?sets = card (\<Union> ?sets)"
+  have card_double: "2 * card ?sets = card (\<Union>?sets)"
   proof (rule card_partition)
     show "finite ?sets" by simp
     { fix i assume "i < n"
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -20,7 +20,7 @@
 class topological_space = "open" +
   assumes open_UNIV [simp, intro]: "open UNIV"
   assumes open_Int [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)"
-  assumes open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union> K)"
+  assumes open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union>K)"
 begin
 
 definition
@@ -66,7 +66,7 @@
 lemma closed_INT [continuous_intros, intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)"
   unfolding closed_def by auto
 
-lemma closed_Inter [continuous_intros, intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)"
+lemma closed_Inter [continuous_intros, intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter>K)"
   unfolding closed_def uminus_Inf by auto
 
 lemma closed_Union [continuous_intros, intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
@@ -1067,12 +1067,12 @@
       by (auto simp: decseq_def)
     show "\<And>n. x \<in> (\<Inter>i\<le>n. A i)" "\<And>n. open (\<Inter>i\<le>n. A i)"
       using A by auto
-    show "nhds x = (INF n. principal (\<Inter> i\<le>n. A i))"
+    show "nhds x = (INF n. principal (\<Inter>i\<le>n. A i))"
       using A unfolding nhds_def
       apply (intro INF_eq)
       apply simp_all
       apply force
-      apply (intro exI[of _ "\<Inter> i\<le>n. A i" for n] conjI open_INT)
+      apply (intro exI[of _ "\<Inter>i\<le>n. A i" for n] conjI open_INT)
       apply auto
       done
   qed
@@ -1521,7 +1521,7 @@
     "compact S \<longleftrightarrow> (\<forall>C. (\<forall>c\<in>C. open c) \<and> S \<subseteq> \<Union>C \<longrightarrow> (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
 
 lemma compactI:
-  assumes "\<And>C. \<forall>t\<in>C. open t \<Longrightarrow> s \<subseteq> \<Union> C \<Longrightarrow> \<exists>C'. C' \<subseteq> C \<and> finite C' \<and> s \<subseteq> \<Union> C'"
+  assumes "\<And>C. \<forall>t\<in>C. open t \<Longrightarrow> s \<subseteq> \<Union>C \<Longrightarrow> \<exists>C'. C' \<subseteq> C \<and> finite C' \<and> s \<subseteq> \<Union>C'"
   shows "compact s"
   unfolding compact_eq_heine_borel using assms by metis
 
@@ -1584,8 +1584,8 @@
 qed
 
 lemma compact_imp_fip:
-  "compact s \<Longrightarrow> \<forall>t \<in> f. closed t \<Longrightarrow> \<forall>f'. finite f' \<and> f' \<subseteq> f \<longrightarrow> (s \<inter> (\<Inter> f') \<noteq> {}) \<Longrightarrow>
-    s \<inter> (\<Inter> f) \<noteq> {}"
+  "compact s \<Longrightarrow> \<forall>t \<in> f. closed t \<Longrightarrow> \<forall>f'. finite f' \<and> f' \<subseteq> f \<longrightarrow> (s \<inter> (\<Inter>f') \<noteq> {}) \<Longrightarrow>
+    s \<inter> (\<Inter>f) \<noteq> {}"
   unfolding compact_fip by auto
 
 lemma compact_imp_fip_image:
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/ZF/Games.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -831,10 +831,10 @@
   Pg_less_def: "G < H \<longleftrightarrow> G \<le> H \<and> G \<noteq> (H::Pg)"
 
 definition
-  Pg_minus_def: "- G = the_elem (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
+  Pg_minus_def: "- G = the_elem (\<Union>g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
 
 definition
-  Pg_plus_def: "G + H = the_elem (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})"
+  Pg_plus_def: "G + H = the_elem (\<Union>g \<in> Rep_Pg G. \<Union>h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})"
 
 definition
   Pg_diff_def: "G - H = G + (- (H::Pg))"