tuned whitespace;
authorwenzelm
Fri Jun 26 10:20:33 2015 +0200 (2015-06-26)
changeset 6058548fdff264eb2
parent 60583 a645a0e6d790
child 60586 1d31e3a50373
tuned whitespace;
src/HOL/Algebra/Lattice.thy
src/HOL/BNF_Cardinal_Order_Relation.thy
src/HOL/BNF_Wellorder_Embedding.thy
src/HOL/BNF_Wellorder_Relation.thy
src/HOL/Cardinals/Cardinal_Arithmetic.thy
src/HOL/Cardinals/Cardinal_Order_Relation.thy
src/HOL/Cardinals/Order_Relation_More.thy
src/HOL/Cardinals/Wellorder_Embedding.thy
src/HOL/Cardinals/Wellorder_Relation.thy
src/HOL/Complete_Lattices.thy
src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy
src/HOL/Datatype_Examples/Lambda_Term.thy
src/HOL/Finite_Set.thy
src/HOL/HOLCF/Cont.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Hoare/SchorrWaite.thy
src/HOL/Library/Indicator_Function.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Nominal/Examples/Class2.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Projective_Limit.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Probability/ex/Dining_Cryptographers.thy
src/HOL/Topological_Spaces.thy
src/HOL/ZF/Games.thy
     1.1 --- a/src/HOL/Algebra/Lattice.thy	Fri Jun 26 00:14:10 2015 +0200
     1.2 +++ b/src/HOL/Algebra/Lattice.thy	Fri Jun 26 10:20:33 2015 +0200
     1.3 @@ -589,7 +589,7 @@
     1.4  lemma (in weak_upper_semilattice) finite_sup_insertI:
     1.5    assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
     1.6      and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
     1.7 -  shows "P (\<Squnion> (insert x A))"
     1.8 +  shows "P (\<Squnion>(insert x A))"
     1.9  proof (cases "A = {}")
    1.10    case True with P and xA show ?thesis
    1.11      by (simp add: finite_sup_least)
    1.12 @@ -828,7 +828,7 @@
    1.13  lemma (in weak_lower_semilattice) finite_inf_insertI:
    1.14    assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
    1.15      and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
    1.16 -  shows "P (\<Sqinter> (insert x A))"
    1.17 +  shows "P (\<Sqinter>(insert x A))"
    1.18  proof (cases "A = {}")
    1.19    case True with P and xA show ?thesis
    1.20      by (simp add: finite_inf_greatest)
    1.21 @@ -856,7 +856,7 @@
    1.22  
    1.23  lemma (in weak_lower_semilattice) inf_of_two_greatest:
    1.24    "[| x \<in> carrier L; y \<in> carrier L |] ==>
    1.25 -  greatest L (\<Sqinter> {x, y}) (Lower L {x, y})"
    1.26 +  greatest L (\<Sqinter>{x, y}) (Lower L {x, y})"
    1.27  proof (unfold inf_def)
    1.28    assume L: "x \<in> carrier L"  "y \<in> carrier L"
    1.29    with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast
    1.30 @@ -904,8 +904,8 @@
    1.31  proof -
    1.32    (* FIXME: improved simp, see weak_join_assoc above *)
    1.33    have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
    1.34 -  also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma)
    1.35 -  also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
    1.36 +  also from L have "... .= \<Sqinter>{z, x, y}" by (simp add: weak_meet_assoc_lemma)
    1.37 +  also from L have "... = \<Sqinter>{x, y, z}" by (simp add: insert_commute)
    1.38    also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric])
    1.39    finally show ?thesis by (simp add: L)
    1.40  qed
    1.41 @@ -1286,15 +1286,15 @@
    1.42  next
    1.43    fix B
    1.44    assume "B \<subseteq> carrier ?L"
    1.45 -  then have "least ?L (\<Union> B) (Upper ?L B)"
    1.46 +  then have "least ?L (\<Union>B) (Upper ?L B)"
    1.47      by (fastforce intro!: least_UpperI simp: Upper_def)
    1.48    then show "EX s. least ?L s (Upper ?L B)" ..
    1.49  next
    1.50    fix B
    1.51    assume "B \<subseteq> carrier ?L"
    1.52 -  then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
    1.53 -    txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
    1.54 -      @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
    1.55 +  then have "greatest ?L (\<Inter>B \<inter> A) (Lower ?L B)"
    1.56 +    txt {* @{term "\<Inter>B"} is not the infimum of @{term B}:
    1.57 +      @{term "\<Inter>{} = UNIV"} which is in general bigger than @{term "A"}! *}
    1.58      by (fastforce intro!: greatest_LowerI simp: Lower_def)
    1.59    then show "EX i. greatest ?L i (Lower ?L B)" ..
    1.60  qed
     2.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Fri Jun 26 00:14:10 2015 +0200
     2.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Fri Jun 26 10:20:33 2015 +0200
     2.3 @@ -1051,10 +1051,10 @@
     2.4  lemma card_of_UNION_ordLeq_infinite:
     2.5  assumes INF: "\<not>finite B" and
     2.6          LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
     2.7 -shows "|\<Union> i \<in> I. A i| \<le>o |B|"
     2.8 +shows "|\<Union>i \<in> I. A i| \<le>o |B|"
     2.9  proof(cases "I = {}", simp add: card_of_empty)
    2.10    assume *: "I \<noteq> {}"
    2.11 -  have "|\<Union> i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
    2.12 +  have "|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
    2.13    using card_of_UNION_Sigma by blast
    2.14    moreover have "|SIGMA i : I. A i| \<le>o |B|"
    2.15    using assms card_of_Sigma_ordLeq_infinite by blast
    2.16 @@ -1064,14 +1064,14 @@
    2.17  corollary card_of_UNION_ordLeq_infinite_Field:
    2.18  assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
    2.19          LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
    2.20 -shows "|\<Union> i \<in> I. A i| \<le>o r"
    2.21 +shows "|\<Union>i \<in> I. A i| \<le>o r"
    2.22  proof-
    2.23    let ?B  = "Field r"
    2.24    have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso
    2.25    ordIso_symmetric by blast
    2.26    hence "|I| \<le>o |?B|"  "\<forall>i \<in> I. |A i| \<le>o |?B|"
    2.27    using LEQ_I LEQ ordLeq_ordIso_trans by blast+
    2.28 -  hence  "|\<Union> i \<in> I. A i| \<le>o |?B|" using INF LEQ
    2.29 +  hence  "|\<Union>i \<in> I. A i| \<le>o |?B|" using INF LEQ
    2.30    card_of_UNION_ordLeq_infinite by blast
    2.31    thus ?thesis using 1 ordLeq_ordIso_trans by blast
    2.32  qed
     3.1 --- a/src/HOL/BNF_Wellorder_Embedding.thy	Fri Jun 26 00:14:10 2015 +0200
     3.2 +++ b/src/HOL/BNF_Wellorder_Embedding.thy	Fri Jun 26 10:20:33 2015 +0200
     3.3 @@ -26,7 +26,7 @@
     3.4  assumes WELL: "Well_order r" and
     3.5          OF: "\<And> i. i \<in> I \<Longrightarrow> wo_rel.ofilter r (A i)" and
     3.6         INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
     3.7 -shows "inj_on f (\<Union> i \<in> I. A i)"
     3.8 +shows "inj_on f (\<Union>i \<in> I. A i)"
     3.9  proof-
    3.10    have "wo_rel r" using WELL by (simp add: wo_rel_def)
    3.11    hence "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i <= A j \<or> A j <= A i"
    3.12 @@ -487,7 +487,7 @@
    3.13    have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
    3.14    have OF: "wo_rel.ofilter r (underS r a)"
    3.15    by (auto simp add: Well wo_rel.underS_ofilter)
    3.16 -  hence UN: "underS r a = (\<Union>  b \<in> underS r a. under r b)"
    3.17 +  hence UN: "underS r a = (\<Union>b \<in> underS r a. under r b)"
    3.18    using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast
    3.19    (* Gather facts about elements of underS r a *)
    3.20    {fix b assume *: "b \<in> underS r a"
    3.21 @@ -520,13 +520,13 @@
    3.22    (*  *)
    3.23    have OF': "wo_rel.ofilter r' (f`(underS r a))"
    3.24    proof-
    3.25 -    have "f`(underS r a) = f`(\<Union>  b \<in> underS r a. under r b)"
    3.26 +    have "f`(underS r a) = f`(\<Union>b \<in> underS r a. under r b)"
    3.27      using UN by auto
    3.28 -    also have "\<dots> = (\<Union>  b \<in> underS r a. f`(under r b))" by blast
    3.29 -    also have "\<dots> = (\<Union>  b \<in> underS r a. (under r' (f b)))"
    3.30 +    also have "\<dots> = (\<Union>b \<in> underS r a. f`(under r b))" by blast
    3.31 +    also have "\<dots> = (\<Union>b \<in> underS r a. (under r' (f b)))"
    3.32      using bFact by auto
    3.33      finally
    3.34 -    have "f`(underS r a) = (\<Union>  b \<in> underS r a. (under r' (f b)))" .
    3.35 +    have "f`(underS r a) = (\<Union>b \<in> underS r a. (under r' (f b)))" .
    3.36      thus ?thesis
    3.37      using Well' bFact
    3.38            wo_rel.ofilter_UNION[of r' "underS r a" "\<lambda> b. under r' (f b)"] by fastforce
     4.1 --- a/src/HOL/BNF_Wellorder_Relation.thy	Fri Jun 26 00:14:10 2015 +0200
     4.2 +++ b/src/HOL/BNF_Wellorder_Relation.thy	Fri Jun 26 10:20:33 2015 +0200
     4.3 @@ -478,20 +478,20 @@
     4.4  qed
     4.5  
     4.6  lemma ofilter_UNION:
     4.7 -"(\<And> i. i \<in> I \<Longrightarrow> ofilter(A i)) \<Longrightarrow> ofilter (\<Union> i \<in> I. A i)"
     4.8 +"(\<And> i. i \<in> I \<Longrightarrow> ofilter(A i)) \<Longrightarrow> ofilter (\<Union>i \<in> I. A i)"
     4.9  unfolding ofilter_def by blast
    4.10  
    4.11  lemma ofilter_under_UNION:
    4.12  assumes "ofilter A"
    4.13 -shows "A = (\<Union> a \<in> A. under a)"
    4.14 +shows "A = (\<Union>a \<in> A. under a)"
    4.15  proof
    4.16    have "\<forall>a \<in> A. under a \<le> A"
    4.17    using assms ofilter_def by auto
    4.18 -  thus "(\<Union> a \<in> A. under a) \<le> A" by blast
    4.19 +  thus "(\<Union>a \<in> A. under a) \<le> A" by blast
    4.20  next
    4.21    have "\<forall>a \<in> A. a \<in> under a"
    4.22    using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast
    4.23 -  thus "A \<le> (\<Union> a \<in> A. under a)" by blast
    4.24 +  thus "A \<le> (\<Union>a \<in> A. under a)" by blast
    4.25  qed
    4.26  
    4.27  subsubsection{* Other properties *}
     5.1 --- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Fri Jun 26 00:14:10 2015 +0200
     5.2 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Fri Jun 26 10:20:33 2015 +0200
     5.3 @@ -297,8 +297,8 @@
     5.4  assumes "|A| \<le>o k" and "\<forall> a \<in> A. |vimage f {a}| \<le>o k" and "Cinfinite k"
     5.5  shows "|vimage f A| \<le>o k"
     5.6  proof-
     5.7 -  have "vimage f A = (\<Union> a \<in> A. vimage f {a})" by auto
     5.8 -  also have "|\<Union> a \<in> A. vimage f {a}| \<le>o k"
     5.9 +  have "vimage f A = (\<Union>a \<in> A. vimage f {a})" by auto
    5.10 +  also have "|\<Union>a \<in> A. vimage f {a}| \<le>o k"
    5.11    using UNION_Cinfinite_bound[OF assms] .
    5.12    finally show ?thesis .
    5.13  qed
     6.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Fri Jun 26 00:14:10 2015 +0200
     6.2 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Fri Jun 26 10:20:33 2015 +0200
     6.3 @@ -715,7 +715,7 @@
     6.4  lemma lists_def2: "lists A = {l. set l \<le> A}"
     6.5  using in_listsI by blast
     6.6  
     6.7 -lemma lists_UNION_nlists: "lists A = (\<Union> n. nlists A n)"
     6.8 +lemma lists_UNION_nlists: "lists A = (\<Union>n. nlists A n)"
     6.9  unfolding lists_def2 nlists_def by blast
    6.10  
    6.11  lemma card_of_lists: "|A| \<le>o |lists A|"
    6.12 @@ -1455,7 +1455,7 @@
    6.13  unfolding Func_option_def Pfunc_def by auto
    6.14  
    6.15  lemma Pfunc_Func_option:
    6.16 -"Pfunc A B = (\<Union> A' \<in> Pow A. Func_option A' B)"
    6.17 +"Pfunc A B = (\<Union>A' \<in> Pow A. Func_option A' B)"
    6.18  proof safe
    6.19    fix f assume f: "f \<in> Pfunc A B"
    6.20    show "f \<in> (\<Union>A'\<in>Pow A. Func_option A' B)"
    6.21 @@ -1504,7 +1504,7 @@
    6.22  assumes "B \<noteq> {}"
    6.23  shows "|Pfunc A B| \<le>o |Pow A <*> Func_option A B|"
    6.24  proof-
    6.25 -  have "|Pfunc A B| =o |\<Union> A' \<in> Pow A. Func_option A' B|" (is "_ =o ?K")
    6.26 +  have "|Pfunc A B| =o |\<Union>A' \<in> Pow A. Func_option A' B|" (is "_ =o ?K")
    6.27      unfolding Pfunc_Func_option by(rule card_of_refl)
    6.28    also have "?K \<le>o |Sigma (Pow A) (\<lambda> A'. Func_option A' B)|" using card_of_UNION_Sigma .
    6.29    also have "|Sigma (Pow A) (\<lambda> A'. Func_option A' B)| \<le>o |Pow A <*> Func_option A B|"
    6.30 @@ -1635,14 +1635,14 @@
    6.31  qed
    6.32  
    6.33  lemma relChain_stabilize:
    6.34 -assumes rc: "relChain r As" and AsB: "(\<Union> i \<in> Field r. As i) \<subseteq> B" and Br: "|B| <o r"
    6.35 +assumes rc: "relChain r As" and AsB: "(\<Union>i \<in> Field r. As i) \<subseteq> B" and Br: "|B| <o r"
    6.36  and ir: "\<not>finite (Field r)" and cr: "Card_order r"
    6.37  shows "\<exists> i \<in> Field r. As (succ r i) = As i"
    6.38  proof(rule ccontr, auto)
    6.39    have 0: "wo_rel r" and 00: "Well_order r"
    6.40    unfolding wo_rel_def by (metis card_order_on_well_order_on cr)+
    6.41    have L: "isLimOrd r" using ir cr by (metis card_order_infinite_isLimOrd)
    6.42 -  have AsBs: "(\<Union> i \<in> Field r. As (succ r i)) \<subseteq> B"
    6.43 +  have AsBs: "(\<Union>i \<in> Field r. As (succ r i)) \<subseteq> B"
    6.44    using AsB L apply safe by (metis "0" UN_I set_mp wo_rel.isLimOrd_succ)
    6.45    assume As_s: "\<forall>i\<in>Field r. As (succ r i) \<noteq> As i"
    6.46    have 1: "\<forall>i j. (i,j) \<in> r \<and> i \<noteq> j \<longrightarrow> As i \<subset> As j"
    6.47 @@ -1719,7 +1719,7 @@
    6.48     obtain j0 where j0: "j0 \<in> Field r" using Fi by auto
    6.49     def g \<equiv> "\<lambda> a. if F a \<noteq> {} then gg a else j0"
    6.50     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
    6.51 -   hence 1: "Field r \<subseteq> (\<Union> a \<in> A. under r (g a))"
    6.52 +   hence 1: "Field r \<subseteq> (\<Union>a \<in> A. under r (g a))"
    6.53     using f[symmetric] unfolding under_def image_def by auto
    6.54     have gA: "g ` A \<subseteq> Field r" using gg j0 unfolding Field_def g_def by auto
    6.55     moreover have "cofinal (g ` A) r" unfolding cofinal_def proof safe
    6.56 @@ -1751,10 +1751,10 @@
    6.57    {assume Kr: "|K| <o r"
    6.58     then obtain f where "\<forall> a \<in> Field r. f a \<in> K \<and> a \<noteq> f a \<and> (a, f a) \<in> r"
    6.59     using cof unfolding cofinal_def by metis
    6.60 -   hence "Field r \<subseteq> (\<Union> a \<in> K. underS r a)" unfolding underS_def by auto
    6.61 -   hence "r \<le>o |\<Union> a \<in> K. underS r a|" using cr
    6.62 +   hence "Field r \<subseteq> (\<Union>a \<in> K. underS r a)" unfolding underS_def by auto
    6.63 +   hence "r \<le>o |\<Union>a \<in> K. underS r a|" using cr
    6.64     by (metis Card_order_iff_ordLeq_card_of card_of_mono1 ordLeq_transitive)
    6.65 -   also have "|\<Union> a \<in> K. underS r a| \<le>o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma)
    6.66 +   also have "|\<Union>a \<in> K. underS r a| \<le>o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma)
    6.67     also
    6.68     {have "\<forall> a \<in> K. |underS r a| <o r" using K by (metis card_of_underS cr subsetD)
    6.69      hence "|SIGMA a: K. underS r a| <o r" using st Kr unfolding stable_def by auto
    6.70 @@ -1818,9 +1818,9 @@
    6.71  lemma stable_UNION:
    6.72  assumes ST: "stable r" and A_LESS: "|A| <o r" and
    6.73          F_LESS: "\<And> a. a \<in> A \<Longrightarrow> |F a| <o r"
    6.74 -shows "|\<Union> a \<in> A. F a| <o r"
    6.75 +shows "|\<Union>a \<in> A. F a| <o r"
    6.76  proof-
    6.77 -  have "|\<Union> a \<in> A. F a| \<le>o |SIGMA a : A. F a|"
    6.78 +  have "|\<Union>a \<in> A. F a| \<le>o |SIGMA a : A. F a|"
    6.79    using card_of_UNION_Sigma by blast
    6.80    thus ?thesis using assms stable_elim ordLeq_ordLess_trans by blast
    6.81  qed
     7.1 --- a/src/HOL/Cardinals/Order_Relation_More.thy	Fri Jun 26 00:14:10 2015 +0200
     7.2 +++ b/src/HOL/Cardinals/Order_Relation_More.thy	Fri Jun 26 10:20:33 2015 +0200
     7.3 @@ -133,12 +133,12 @@
     7.4  
     7.5  lemma Refl_under_Under:
     7.6  assumes REFL: "Refl r" and NE: "A \<noteq> {}"
     7.7 -shows "Under r A = (\<Inter> a \<in> A. under r a)"
     7.8 +shows "Under r A = (\<Inter>a \<in> A. under r a)"
     7.9  proof
    7.10 -  show "Under r A \<subseteq> (\<Inter> a \<in> A. under r a)"
    7.11 +  show "Under r A \<subseteq> (\<Inter>a \<in> A. under r a)"
    7.12    by(unfold Under_def under_def, auto)
    7.13  next
    7.14 -  show "(\<Inter> a \<in> A. under r a) \<subseteq> Under r A"
    7.15 +  show "(\<Inter>a \<in> A. under r a) \<subseteq> Under r A"
    7.16    proof(auto)
    7.17      fix x
    7.18      assume *: "\<forall>xa \<in> A. x \<in> under r xa"
    7.19 @@ -157,12 +157,12 @@
    7.20  
    7.21  lemma Refl_underS_UnderS:
    7.22  assumes REFL: "Refl r" and NE: "A \<noteq> {}"
    7.23 -shows "UnderS r A = (\<Inter> a \<in> A. underS r a)"
    7.24 +shows "UnderS r A = (\<Inter>a \<in> A. underS r a)"
    7.25  proof
    7.26 -  show "UnderS r A \<subseteq> (\<Inter> a \<in> A. underS r a)"
    7.27 +  show "UnderS r A \<subseteq> (\<Inter>a \<in> A. underS r a)"
    7.28    by(unfold UnderS_def underS_def, auto)
    7.29  next
    7.30 -  show "(\<Inter> a \<in> A. underS r a) \<subseteq> UnderS r A"
    7.31 +  show "(\<Inter>a \<in> A. underS r a) \<subseteq> UnderS r A"
    7.32    proof(auto)
    7.33      fix x
    7.34      assume *: "\<forall>xa \<in> A. x \<in> underS r xa"
    7.35 @@ -181,12 +181,12 @@
    7.36  
    7.37  lemma Refl_above_Above:
    7.38  assumes REFL: "Refl r" and NE: "A \<noteq> {}"
    7.39 -shows "Above r A = (\<Inter> a \<in> A. above r a)"
    7.40 +shows "Above r A = (\<Inter>a \<in> A. above r a)"
    7.41  proof
    7.42 -  show "Above r A \<subseteq> (\<Inter> a \<in> A. above r a)"
    7.43 +  show "Above r A \<subseteq> (\<Inter>a \<in> A. above r a)"
    7.44    by(unfold Above_def above_def, auto)
    7.45  next
    7.46 -  show "(\<Inter> a \<in> A. above r a) \<subseteq> Above r A"
    7.47 +  show "(\<Inter>a \<in> A. above r a) \<subseteq> Above r A"
    7.48    proof(auto)
    7.49      fix x
    7.50      assume *: "\<forall>xa \<in> A. x \<in> above r xa"
    7.51 @@ -205,12 +205,12 @@
    7.52  
    7.53  lemma Refl_aboveS_AboveS:
    7.54  assumes REFL: "Refl r" and NE: "A \<noteq> {}"
    7.55 -shows "AboveS r A = (\<Inter> a \<in> A. aboveS r a)"
    7.56 +shows "AboveS r A = (\<Inter>a \<in> A. aboveS r a)"
    7.57  proof
    7.58 -  show "AboveS r A \<subseteq> (\<Inter> a \<in> A. aboveS r a)"
    7.59 +  show "AboveS r A \<subseteq> (\<Inter>a \<in> A. aboveS r a)"
    7.60    by(unfold AboveS_def aboveS_def, auto)
    7.61  next
    7.62 -  show "(\<Inter> a \<in> A. aboveS r a) \<subseteq> AboveS r A"
    7.63 +  show "(\<Inter>a \<in> A. aboveS r a) \<subseteq> AboveS r A"
    7.64    proof(auto)
    7.65      fix x
    7.66      assume *: "\<forall>xa \<in> A. x \<in> aboveS r xa"
     8.1 --- a/src/HOL/Cardinals/Wellorder_Embedding.thy	Fri Jun 26 00:14:10 2015 +0200
     8.2 +++ b/src/HOL/Cardinals/Wellorder_Embedding.thy	Fri Jun 26 10:20:33 2015 +0200
     8.3 @@ -17,7 +17,7 @@
     8.4  assumes WELL: "Well_order r" and
     8.5          OF: "\<And> i. i \<in> I \<Longrightarrow> ofilter r (A i)" and
     8.6         BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
     8.7 -shows "bij_betw f (\<Union> i \<in> I. A i) (\<Union> i \<in> I. A' i)"
     8.8 +shows "bij_betw f (\<Union>i \<in> I. A i) (\<Union>i \<in> I. A' i)"
     8.9  proof-
    8.10    have "wo_rel r" using WELL by (simp add: wo_rel_def)
    8.11    hence "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i"
     9.1 --- a/src/HOL/Cardinals/Wellorder_Relation.thy	Fri Jun 26 00:14:10 2015 +0200
     9.2 +++ b/src/HOL/Cardinals/Wellorder_Relation.thy	Fri Jun 26 10:20:33 2015 +0200
     9.3 @@ -437,7 +437,7 @@
     9.4  unfolding ofilter_def by blast
     9.5  
     9.6  lemma ofilter_INTER:
     9.7 -"\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter> i \<in> I. A i)"
     9.8 +"\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter>i \<in> I. A i)"
     9.9  unfolding ofilter_def by blast
    9.10  
    9.11  lemma ofilter_Inter:
    10.1 --- a/src/HOL/Complete_Lattices.thy	Fri Jun 26 00:14:10 2015 +0200
    10.2 +++ b/src/HOL/Complete_Lattices.thy	Fri Jun 26 10:20:33 2015 +0200
    10.3 @@ -1204,7 +1204,7 @@
    10.4    "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
    10.5    by (fact Sup_image_eq)
    10.6  
    10.7 -lemma Union_SetCompr_eq: "\<Union> {f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}"
    10.8 +lemma Union_SetCompr_eq: "\<Union>{f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}"
    10.9    by blast
   10.10  
   10.11  lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<exists>x\<in>A. b \<in> B x)"
   10.12 @@ -1360,7 +1360,7 @@
   10.13  lemma inj_on_UNION_chain:
   10.14    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
   10.15           INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
   10.16 -  shows "inj_on f (\<Union> i \<in> I. A i)"
   10.17 +  shows "inj_on f (\<Union>i \<in> I. A i)"
   10.18  proof -
   10.19    {
   10.20      fix i j x y
   10.21 @@ -1390,11 +1390,11 @@
   10.22  lemma bij_betw_UNION_chain:
   10.23    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
   10.24           BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
   10.25 -  shows "bij_betw f (\<Union> i \<in> I. A i) (\<Union> i \<in> I. A' i)"
   10.26 +  shows "bij_betw f (\<Union>i \<in> I. A i) (\<Union>i \<in> I. A' i)"
   10.27  proof (unfold bij_betw_def, auto)
   10.28    have "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
   10.29    using BIJ bij_betw_def[of f] by auto
   10.30 -  thus "inj_on f (\<Union> i \<in> I. A i)"
   10.31 +  thus "inj_on f (\<Union>i \<in> I. A i)"
   10.32    using CH inj_on_UNION_chain[of I A f] by auto
   10.33  next
   10.34    fix i x
    11.1 --- a/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy	Fri Jun 26 00:14:10 2015 +0200
    11.2 +++ b/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy	Fri Jun 26 10:20:33 2015 +0200
    11.3 @@ -257,7 +257,7 @@
    11.4  qed
    11.5  
    11.6  corollary Fr_subtr:
    11.7 -"Fr ns tr = \<Union> {Fr ns tr' | tr'. subtr ns tr' tr}"
    11.8 +"Fr ns tr = \<Union>{Fr ns tr' | tr'. subtr ns tr' tr}"
    11.9  unfolding Fr_def proof safe
   11.10    fix t assume t: "inFr ns tr t"  hence "root tr \<in> ns" by (rule inFr_root_in)
   11.11    thus "t \<in> \<Union>{{t. inFr ns tr' t} |tr'. subtr ns tr' tr}"
   11.12 @@ -272,7 +272,7 @@
   11.13    by (metis (lifting) subtr.Step)
   11.14  
   11.15  corollary Fr_subtr_cont:
   11.16 -"Fr ns tr = \<Union> {Inl -` cont tr' | tr'. subtr ns tr' tr}"
   11.17 +"Fr ns tr = \<Union>{Inl -` cont tr' | tr'. subtr ns tr' tr}"
   11.18  unfolding Fr_def
   11.19  apply safe
   11.20  apply (frule inFr_subtr)
   11.21 @@ -290,7 +290,7 @@
   11.22  qed
   11.23  
   11.24  corollary Itr_subtr:
   11.25 -"Itr ns tr = \<Union> {Itr ns tr' | tr'. subtr ns tr' tr}"
   11.26 +"Itr ns tr = \<Union>{Itr ns tr' | tr'. subtr ns tr' tr}"
   11.27  unfolding Itr_def apply safe
   11.28  apply (metis (lifting, mono_tags) UnionI inItr_root_in mem_Collect_eq subtr.Refl)
   11.29  by (metis subtr_inItr)
   11.30 @@ -1121,7 +1121,7 @@
   11.31  assumes r: "regular tr" and In: "root tr \<in> ns"
   11.32  shows "Fr ns tr =
   11.33         Inl -` (cont tr) \<union>
   11.34 -       \<Union> {Fr (ns - {root tr}) tr' | tr'. Inr tr' \<in> cont tr}"
   11.35 +       \<Union>{Fr (ns - {root tr}) tr' | tr'. Inr tr' \<in> cont tr}"
   11.36  unfolding Fr_def
   11.37  using In inFr.Base regular_inFr[OF assms] apply safe
   11.38  apply (simp, metis (full_types) mem_Collect_eq)
   11.39 @@ -1161,7 +1161,7 @@
   11.40  lemma Lr_rec_in:
   11.41  assumes n: "n \<in> ns"
   11.42  shows "Lr ns n \<subseteq>
   11.43 -{Inl -` tns \<union> (\<Union> {K n' | n'. Inr n' \<in> tns}) | tns K.
   11.44 +{Inl -` tns \<union> (\<Union>{K n' | n'. Inr n' \<in> tns}) | tns K.
   11.45      (n,tns) \<in> P \<and>
   11.46      (\<forall> n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> Lr (ns - {n}) n')}"
   11.47  (is "Lr ns n \<subseteq> {?F tns K | tns K. (n,tns) \<in> P \<and> ?\<phi> tns K}")
   11.48 @@ -1207,7 +1207,7 @@
   11.49  lemma L_rec_in:
   11.50  assumes n: "n \<in> ns"
   11.51  shows "
   11.52 -{Inl -` tns \<union> (\<Union> {K n' | n'. Inr n' \<in> tns}) | tns K.
   11.53 +{Inl -` tns \<union> (\<Union>{K n' | n'. Inr n' \<in> tns}) | tns K.
   11.54      (n,tns) \<in> P \<and>
   11.55      (\<forall> n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> L (ns - {n}) n')}
   11.56   \<subseteq> L ns n"
   11.57 @@ -1247,7 +1247,7 @@
   11.58  function LL where
   11.59  "LL ns n =
   11.60   (if n \<notin> ns then {{}} else
   11.61 - {Inl -` tns \<union> (\<Union> {K n' | n'. Inr n' \<in> tns}) | tns K.
   11.62 + {Inl -` tns \<union> (\<Union>{K n' | n'. Inr n' \<in> tns}) | tns K.
   11.63      (n,tns) \<in> P \<and>
   11.64      (\<forall> n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> LL (ns - {n}) n')})"
   11.65  by(pat_completeness, auto)
    12.1 --- a/src/HOL/Datatype_Examples/Lambda_Term.thy	Fri Jun 26 00:14:10 2015 +0200
    12.2 +++ b/src/HOL/Datatype_Examples/Lambda_Term.thy	Fri Jun 26 10:20:33 2015 +0200
    12.3 @@ -27,14 +27,14 @@
    12.4    "varsOf (Var a) = {a}"
    12.5  | "varsOf (App f x) = varsOf f \<union> varsOf x"
    12.6  | "varsOf (Lam x b) = {x} \<union> varsOf b"
    12.7 -| "varsOf (Lt F t) = varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| fimage (map_prod id varsOf) F})"
    12.8 +| "varsOf (Lt F t) = varsOf t \<union> (\<Union>{{x} \<union> X | x X. (x,X) |\<in>| fimage (map_prod id varsOf) F})"
    12.9  
   12.10  primrec fvarsOf :: "'a trm \<Rightarrow> 'a set" where
   12.11    "fvarsOf (Var x) = {x}"
   12.12  | "fvarsOf (App t1 t2) = fvarsOf t1 \<union> fvarsOf t2"
   12.13  | "fvarsOf (Lam x t) = fvarsOf t - {x}"
   12.14  | "fvarsOf (Lt xts t) = fvarsOf t - {x | x X. (x,X) |\<in>| fimage (map_prod id varsOf) xts} \<union>
   12.15 -    (\<Union> {X | x X. (x,X) |\<in>| fimage (map_prod id varsOf) xts})"
   12.16 +    (\<Union>{X | x X. (x,X) |\<in>| fimage (map_prod id varsOf) xts})"
   12.17  
   12.18  lemma diff_Un_incl_triv: "\<lbrakk>A \<subseteq> D; C \<subseteq> E\<rbrakk> \<Longrightarrow> A - B \<union> C \<subseteq> D \<union> E" by blast
   12.19  
    13.1 --- a/src/HOL/Finite_Set.thy	Fri Jun 26 00:14:10 2015 +0200
    13.2 +++ b/src/HOL/Finite_Set.thy	Fri Jun 26 10:20:33 2015 +0200
    13.3 @@ -1433,7 +1433,7 @@
    13.4  
    13.5  lemma insert_partition:
    13.6    "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
    13.7 -  \<Longrightarrow> x \<inter> \<Union> F = {}"
    13.8 +  \<Longrightarrow> x \<inter> \<Union>F = {}"
    13.9  by auto
   13.10  
   13.11  lemma finite_psubset_induct[consumes 1, case_names psubset]:
   13.12 @@ -1486,13 +1486,13 @@
   13.13  text{* main cardinality theorem *}
   13.14  lemma card_partition [rule_format]:
   13.15    "finite C ==>
   13.16 -     finite (\<Union> C) -->
   13.17 +     finite (\<Union>C) -->
   13.18       (\<forall>c\<in>C. card c = k) -->
   13.19       (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
   13.20 -     k * card(C) = card (\<Union> C)"
   13.21 +     k * card(C) = card (\<Union>C)"
   13.22  apply (erule finite_induct, simp)
   13.23  apply (simp add: card_Un_disjoint insert_partition 
   13.24 -       finite_subset [of _ "\<Union> (insert x F)"])
   13.25 +       finite_subset [of _ "\<Union>(insert x F)"])
   13.26  done
   13.27  
   13.28  lemma card_eq_UNIV_imp_eq_UNIV:
    14.1 --- a/src/HOL/HOLCF/Cont.thy	Fri Jun 26 00:14:10 2015 +0200
    14.2 +++ b/src/HOL/HOLCF/Cont.thy	Fri Jun 26 10:20:33 2015 +0200
    14.3 @@ -91,7 +91,7 @@
    14.4  text {* continuity implies preservation of lubs *}
    14.5  
    14.6  lemma cont2contlubE:
    14.7 -  "\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion> i. Y i) = (\<Squnion> i. f (Y i))"
    14.8 +  "\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))"
    14.9  apply (rule lub_eqI [symmetric])
   14.10  apply (erule (1) contE)
   14.11  done
    15.1 --- a/src/HOL/Hilbert_Choice.thy	Fri Jun 26 00:14:10 2015 +0200
    15.2 +++ b/src/HOL/Hilbert_Choice.thy	Fri Jun 26 10:20:33 2015 +0200
    15.3 @@ -408,20 +408,20 @@
    15.4  qed
    15.5  
    15.6  lemma Ex_inj_on_UNION_Sigma:
    15.7 -  "\<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))"
    15.8 +  "\<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))"
    15.9  proof
   15.10    let ?phi = "\<lambda> a i. i \<in> I \<and> a \<in> A i"
   15.11    let ?sm = "\<lambda> a. SOME i. ?phi a i"
   15.12    let ?f = "\<lambda>a. (?sm a, a)"
   15.13 -  have "inj_on ?f (\<Union> i \<in> I. A i)" unfolding inj_on_def by auto
   15.14 +  have "inj_on ?f (\<Union>i \<in> I. A i)" unfolding inj_on_def by auto
   15.15    moreover
   15.16    { { fix i a assume "i \<in> I" and "a \<in> A i"
   15.17        hence "?sm a \<in> I \<and> a \<in> A(?sm a)" using someI[of "?phi a" i] by auto
   15.18      }
   15.19 -    hence "?f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i)" by auto
   15.20 +    hence "?f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i)" by auto
   15.21    }
   15.22    ultimately
   15.23 -  show "inj_on ?f (\<Union> i \<in> I. A i) \<and> ?f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i)"
   15.24 +  show "inj_on ?f (\<Union>i \<in> I. A i) \<and> ?f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i)"
   15.25    by auto
   15.26  qed
   15.27  
    16.1 --- a/src/HOL/Hoare/SchorrWaite.thy	Fri Jun 26 00:14:10 2015 +0200
    16.2 +++ b/src/HOL/Hoare/SchorrWaite.thy	Fri Jun 26 10:20:33 2015 +0200
    16.3 @@ -17,7 +17,7 @@
    16.4  
    16.5  definition
    16.6    relS :: "('a \<Rightarrow> 'a ref) set \<Rightarrow> ('a \<times> 'a) set"
    16.7 -  where "relS M = (\<Union> m \<in> M. rel m)"
    16.8 +  where "relS M = (\<Union>m \<in> M. rel m)"
    16.9  
   16.10  definition
   16.11    addrs :: "'a ref set \<Rightarrow> 'a set"
    17.1 --- a/src/HOL/Library/Indicator_Function.thy	Fri Jun 26 00:14:10 2015 +0200
    17.2 +++ b/src/HOL/Library/Indicator_Function.thy	Fri Jun 26 10:20:33 2015 +0200
    17.3 @@ -87,18 +87,18 @@
    17.4      by auto
    17.5    then have 
    17.6      "\<And>n. (indicator (A (n + i)) x :: 'a) = 1"
    17.7 -    "(indicator (\<Union> i. A i) x :: 'a) = 1"
    17.8 +    "(indicator (\<Union>i. A i) x :: 'a) = 1"
    17.9      using incseqD[OF \<open>incseq A\<close>, of i "n + i" for n] \<open>x \<in> A i\<close> by (auto simp: indicator_def)
   17.10    then show ?thesis
   17.11      by (rule_tac LIMSEQ_offset[of _ i]) simp
   17.12  qed (auto simp: indicator_def)
   17.13  
   17.14  lemma LIMSEQ_indicator_UN:
   17.15 -  "(\<lambda>k. indicator (\<Union> i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
   17.16 +  "(\<lambda>k. indicator (\<Union>i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
   17.17  proof -
   17.18 -  have "(\<lambda>k. indicator (\<Union> i<k. A i) x::'a) ----> indicator (\<Union>k. \<Union> i<k. A i) x"
   17.19 +  have "(\<lambda>k. indicator (\<Union>i<k. A i) x::'a) ----> indicator (\<Union>k. \<Union>i<k. A i) x"
   17.20      by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans)
   17.21 -  also have "(\<Union>k. \<Union> i<k. A i) = (\<Union>i. A i)"
   17.22 +  also have "(\<Union>k. \<Union>i<k. A i) = (\<Union>i. A i)"
   17.23      by auto
   17.24    finally show ?thesis .
   17.25  qed
   17.26 @@ -123,7 +123,7 @@
   17.27  proof -
   17.28    have "(\<lambda>k. indicator (\<Inter>i<k. A i) x::'a) ----> indicator (\<Inter>k. \<Inter>i<k. A i) x"
   17.29      by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans)
   17.30 -  also have "(\<Inter>k. \<Inter> i<k. A i) = (\<Inter>i. A i)"
   17.31 +  also have "(\<Inter>k. \<Inter>i<k. A i) = (\<Inter>i. A i)"
   17.32      by auto
   17.33    finally show ?thesis .
   17.34  qed
    18.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Fri Jun 26 00:14:10 2015 +0200
    18.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Fri Jun 26 10:20:33 2015 +0200
    18.3 @@ -604,7 +604,7 @@
    18.4  lemma analytic_on_Un: "f analytic_on (s \<union> t) \<longleftrightarrow> f analytic_on s \<and> f analytic_on t"
    18.5    by (auto simp: analytic_on_def)
    18.6  
    18.7 -lemma analytic_on_Union: "f analytic_on (\<Union> s) \<longleftrightarrow> (\<forall>t \<in> s. f analytic_on t)"
    18.8 +lemma analytic_on_Union: "f analytic_on (\<Union>s) \<longleftrightarrow> (\<forall>t \<in> s. f analytic_on t)"
    18.9    by (auto simp: analytic_on_def)
   18.10  
   18.11  lemma analytic_on_UN: "f analytic_on (\<Union>i\<in>I. s i) \<longleftrightarrow> (\<forall>i\<in>I. f analytic_on (s i))"
    19.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jun 26 00:14:10 2015 +0200
    19.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jun 26 10:20:33 2015 +0200
    19.3 @@ -384,7 +384,7 @@
    19.4  lemma affine_UNIV[intro]: "affine UNIV"
    19.5    unfolding affine_def by auto
    19.6  
    19.7 -lemma affine_Inter[intro]: "(\<forall>s\<in>f. affine s) \<Longrightarrow> affine (\<Inter> f)"
    19.8 +lemma affine_Inter[intro]: "(\<forall>s\<in>f. affine s) \<Longrightarrow> affine (\<Inter>f)"
    19.9    unfolding affine_def by auto
   19.10  
   19.11  lemma affine_Int[intro]: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)"
   19.12 @@ -4552,7 +4552,7 @@
   19.13    shows "\<exists>a. a \<noteq> 0 \<and> (\<forall>x\<in>s. 0 \<le> inner a x)"
   19.14  proof -
   19.15    let ?k = "\<lambda>c. {x::'a. 0 \<le> inner c x}"
   19.16 -  have "frontier (cball 0 1) \<inter> (\<Inter> (?k ` s)) \<noteq> {}"
   19.17 +  have "frontier (cball 0 1) \<inter> (\<Inter>(?k ` s)) \<noteq> {}"
   19.18      apply (rule compact_imp_fip)
   19.19      apply (rule compact_frontier[OF compact_cball])
   19.20      defer
   19.21 @@ -4758,7 +4758,7 @@
   19.22  lemma convex_halfspace_intersection:
   19.23    fixes s :: "('a::euclidean_space) set"
   19.24    assumes "closed s" "convex s"
   19.25 -  shows "s = \<Inter> {h. s \<subseteq> h \<and> (\<exists>a b. h = {x. inner a x \<le> b})}"
   19.26 +  shows "s = \<Inter>{h. s \<subseteq> h \<and> (\<exists>a b. h = {x. inner a x \<le> b})}"
   19.27    apply (rule set_eqI)
   19.28    apply rule
   19.29    unfolding Inter_iff Ball_def mem_Collect_eq
   19.30 @@ -4935,7 +4935,7 @@
   19.31    fixes f :: "'a::euclidean_space set set"
   19.32    assumes "card f = n"
   19.33      and "n \<ge> DIM('a) + 1"
   19.34 -    and "\<forall>s\<in>f. convex s" "\<forall>t\<subseteq>f. card t = DIM('a) + 1 \<longrightarrow> \<Inter> t \<noteq> {}"
   19.35 +    and "\<forall>s\<in>f. convex s" "\<forall>t\<subseteq>f. card t = DIM('a) + 1 \<longrightarrow> \<Inter>t \<noteq> {}"
   19.36    shows "\<Inter>f \<noteq> {}"
   19.37    using assms
   19.38  proof (induct n arbitrary: f)
   19.39 @@ -5033,7 +5033,7 @@
   19.40  lemma helly:
   19.41    fixes f :: "'a::euclidean_space set set"
   19.42    assumes "card f \<ge> DIM('a) + 1" "\<forall>s\<in>f. convex s"
   19.43 -    and "\<forall>t\<subseteq>f. card t = DIM('a) + 1 \<longrightarrow> \<Inter> t \<noteq> {}"
   19.44 +    and "\<forall>t\<subseteq>f. card t = DIM('a) + 1 \<longrightarrow> \<Inter>t \<noteq> {}"
   19.45    shows "\<Inter>f \<noteq> {}"
   19.46    apply (rule helly_induct)
   19.47    using assms
   19.48 @@ -7756,7 +7756,7 @@
   19.49    have "\<Inter>{closure S |S. S \<in> I} \<le> closure (\<Inter>{rel_interior S |S. S \<in> I})"
   19.50      using convex_closure_rel_interior_inter assms by auto
   19.51    moreover
   19.52 -  have "closure (\<Inter>{rel_interior S |S. S \<in> I}) \<le> closure (\<Inter> I)"
   19.53 +  have "closure (\<Inter>{rel_interior S |S. S \<in> I}) \<le> closure (\<Inter>I)"
   19.54      using rel_interior_inter_aux closure_mono[of "\<Inter>{rel_interior S |S. S \<in> I}" "\<Inter>I"]
   19.55      by auto
   19.56    ultimately show ?thesis
   19.57 @@ -8750,7 +8750,7 @@
   19.58      done
   19.59    ultimately have "convex hull (\<Union>(K ` I)) \<supseteq> K0"
   19.60      unfolding K0_def
   19.61 -    using hull_minimal[of _ "convex hull (\<Union> (K ` I))" "cone"]
   19.62 +    using hull_minimal[of _ "convex hull (\<Union>(K ` I))" "cone"]
   19.63      by blast
   19.64    then have "K0 = convex hull (\<Union>(K ` I))"
   19.65      using geq by auto
    20.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Jun 26 00:14:10 2015 +0200
    20.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Jun 26 10:20:33 2015 +0200
    20.3 @@ -648,7 +648,7 @@
    20.4  lemma gauge_inters:
    20.5    assumes "finite s"
    20.6      and "\<forall>d\<in>s. gauge (f d)"
    20.7 -  shows "gauge (\<lambda>x. \<Inter> {f d x | d. d \<in> s})"
    20.8 +  shows "gauge (\<lambda>x. \<Inter>{f d x | d. d \<in> s})"
    20.9  proof -
   20.10    have *: "\<And>x. {f d x |d. d \<in> s} = (\<lambda>d. f d x) ` s"
   20.11      by auto
   20.12 @@ -871,7 +871,7 @@
   20.13    assumes "finite f"
   20.14      and "f \<noteq> {}"
   20.15      and "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::euclidean_space) set)"
   20.16 -  shows "\<exists>p. p division_of (\<Inter> f)"
   20.17 +  shows "\<exists>p. p division_of (\<Inter>f)"
   20.18    using assms
   20.19  proof (induct f rule: finite_induct)
   20.20    case (insert x f)
   20.21 @@ -1066,7 +1066,7 @@
   20.22        done }
   20.23    then have "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
   20.24      by (meson Diff_subset division_of_subset)
   20.25 -  then have "\<exists>d. d division_of \<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)"
   20.26 +  then have "\<exists>d. d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)"
   20.27      apply -
   20.28      apply (rule elementary_inters [OF finite_imageI[OF p(1)]])
   20.29      apply (auto simp: False elementary_inters [OF finite_imageI[OF p(1)]])
   20.30 @@ -1669,7 +1669,7 @@
   20.31    unfolding fine_def by auto
   20.32  
   20.33  lemma fine_inters:
   20.34 - "(\<lambda>x. \<Inter> {f d x | d.  d \<in> s}) fine p \<longleftrightarrow> (\<forall>d\<in>s. (f d) fine p)"
   20.35 + "(\<lambda>x. \<Inter>{f d x | d.  d \<in> s}) fine p \<longleftrightarrow> (\<forall>d\<in>s. (f d) fine p)"
   20.36    unfolding fine_def by blast
   20.37  
   20.38  lemma fine_union: "d fine p1 \<Longrightarrow> d fine p2 \<Longrightarrow> d fine (p1 \<union> p2)"
   20.39 @@ -1851,7 +1851,7 @@
   20.40        by (blast intro: that)
   20.41    }
   20.42    assume as: "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d)"
   20.43 -  have "P (\<Union> ?A)"
   20.44 +  have "P (\<Union>?A)"
   20.45    proof (rule UN_cases)
   20.46      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)
   20.47        (\<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}"
   20.48 @@ -1926,7 +1926,7 @@
   20.49        qed
   20.50      qed
   20.51    qed
   20.52 -  also have "\<Union> ?A = cbox a b"
   20.53 +  also have "\<Union>?A = cbox a b"
   20.54    proof (rule set_eqI,rule)
   20.55      fix x
   20.56      assume "x \<in> \<Union>?A"
    21.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jun 26 00:14:10 2015 +0200
    21.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jun 26 10:20:33 2015 +0200
    21.3 @@ -413,7 +413,7 @@
    21.4  subsection \<open>General notion of a topology as a value\<close>
    21.5  
    21.6  definition "istopology L \<longleftrightarrow>
    21.7 -  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))"
    21.8 +  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))"
    21.9  
   21.10  typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
   21.11    morphisms "openin" "topology"
   21.12 @@ -462,7 +462,7 @@
   21.13  lemma openin_Int[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<inter> T)"
   21.14    using openin_clauses by simp
   21.15  
   21.16 -lemma openin_Union[intro]: "(\<forall>S \<in>K. openin U S) \<Longrightarrow> openin U (\<Union> K)"
   21.17 +lemma openin_Union[intro]: "(\<forall>S \<in>K. openin U S) \<Longrightarrow> openin U (\<Union>K)"
   21.18    using openin_clauses by simp
   21.19  
   21.20  lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)"
   21.21 @@ -501,13 +501,13 @@
   21.22  lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)"
   21.23    by (auto simp add: Diff_Un closedin_def)
   21.24  
   21.25 -lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union> {A - s|s. s\<in>S}"
   21.26 +lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union>{A - s|s. s\<in>S}"
   21.27    by auto
   21.28  
   21.29  lemma closedin_Inter[intro]:
   21.30    assumes Ke: "K \<noteq> {}"
   21.31      and Kc: "\<forall>S \<in>K. closedin U S"
   21.32 -  shows "closedin U (\<Inter> K)"
   21.33 +  shows "closedin U (\<Inter>K)"
   21.34    using Ke Kc unfolding closedin_def Diff_Inter by auto
   21.35  
   21.36  lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)"
   21.37 @@ -575,7 +575,7 @@
   21.38        by blast
   21.39      have "\<Union>K = (\<Union>Sk) \<inter> V"
   21.40        using Sk by auto
   21.41 -    moreover have "openin U (\<Union> Sk)"
   21.42 +    moreover have "openin U (\<Union>Sk)"
   21.43        using Sk by (auto simp add: subset_eq)
   21.44      ultimately have "?L (\<Union>K)" by blast
   21.45    }
    22.1 --- a/src/HOL/Nominal/Examples/Class2.thy	Fri Jun 26 00:14:10 2015 +0200
    22.2 +++ b/src/HOL/Nominal/Examples/Class2.thy	Fri Jun 26 10:20:33 2015 +0200
    22.3 @@ -2888,8 +2888,8 @@
    22.4    and   X::"('a::pt_name) set set"
    22.5    and   pi2::"coname prm"
    22.6    and   Y::"('b::pt_coname) set set"
    22.7 -  shows "(pi1\<bullet>(\<Inter> X)) = \<Inter> (pi1\<bullet>X)"
    22.8 -  and   "(pi2\<bullet>(\<Inter> Y)) = \<Inter> (pi2\<bullet>Y)"
    22.9 +  shows "(pi1\<bullet>(\<Inter>X)) = \<Inter>(pi1\<bullet>X)"
   22.10 +  and   "(pi2\<bullet>(\<Inter>Y)) = \<Inter>(pi2\<bullet>Y)"
   22.11  apply(auto simp add: perm_set_def)
   22.12  apply(rule_tac x="(rev pi1)\<bullet>x" in exI)
   22.13  apply(perm_simp)
    23.1 --- a/src/HOL/Nominal/Nominal.thy	Fri Jun 26 00:14:10 2015 +0200
    23.2 +++ b/src/HOL/Nominal/Nominal.thy	Fri Jun 26 10:20:33 2015 +0200
    23.3 @@ -1888,9 +1888,9 @@
    23.4    assumes  pt: "pt TYPE('a) TYPE('x)"
    23.5    and      at: "at TYPE ('x)"
    23.6    and      fs: "fs TYPE('a) TYPE('x)"
    23.7 -  shows "((supp x)::'x set) = (\<Inter> {S. finite S \<and> S supports x})"
    23.8 +  shows "((supp x)::'x set) = (\<Inter>{S. finite S \<and> S supports x})"
    23.9  proof (rule equalityI)
   23.10 -  show "((supp x)::'x set) \<subseteq> (\<Inter> {S. finite S \<and> S supports x})"
   23.11 +  show "((supp x)::'x set) \<subseteq> (\<Inter>{S. finite S \<and> S supports x})"
   23.12    proof (clarify)
   23.13      fix S c
   23.14      assume b: "c\<in>((supp x)::'x set)" and "finite (S::'x set)" and "S supports x"
   23.15 @@ -1898,7 +1898,7 @@
   23.16      with b show "c\<in>S" by force
   23.17    qed
   23.18  next
   23.19 -  show "(\<Inter> {S. finite S \<and> S supports x}) \<subseteq> ((supp x)::'x set)"
   23.20 +  show "(\<Inter>{S. finite S \<and> S supports x}) \<subseteq> ((supp x)::'x set)"
   23.21    proof (clarify, simp)
   23.22      fix c
   23.23      assume d: "\<forall>(S::'x set). finite S \<and> S supports x \<longrightarrow> c\<in>S"
    24.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Fri Jun 26 00:14:10 2015 +0200
    24.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Fri Jun 26 10:20:33 2015 +0200
    24.3 @@ -83,7 +83,7 @@
    24.4          by (rule finite_subset) auto }
    24.5      
    24.6      { fix N i n x assume "i \<le> N" "n \<le> N" "x \<in> B i n"
    24.7 -      then have 1: "\<exists>m\<le>N. x \<in> (\<Union> n\<le>N. B m n)" by auto
    24.8 +      then have 1: "\<exists>m\<le>N. x \<in> (\<Union>n\<le>N. B m n)" by auto
    24.9        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
   24.10        moreover
   24.11        def L \<equiv> "LEAST n. x \<in> B (m N x) n"
    25.1 --- a/src/HOL/Probability/Caratheodory.thy	Fri Jun 26 00:14:10 2015 +0200
    25.2 +++ b/src/HOL/Probability/Caratheodory.thy	Fri Jun 26 10:20:33 2015 +0200
    25.3 @@ -804,7 +804,7 @@
    25.4      with Ca Cb have "Ca \<inter> Cb \<subseteq> {{}}" by auto
    25.5      then have C_Int_cases: "Ca \<inter> Cb = {{}} \<or> Ca \<inter> Cb = {}" by auto
    25.6  
    25.7 -    from `a \<inter> b = {}` have "\<mu>' (\<Union> (Ca \<union> Cb)) = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c)"
    25.8 +    from `a \<inter> b = {}` have "\<mu>' (\<Union>(Ca \<union> Cb)) = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c)"
    25.9        using Ca Cb by (intro \<mu>') (auto intro!: disjoint_union)
   25.10      also have "\<dots> = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c) + (\<Sum>c\<in>Ca \<inter> Cb. \<mu> c)"
   25.11        using C_Int_cases volume_empty[OF `volume M \<mu>`] by (elim disjE) simp_all
   25.12 @@ -915,7 +915,7 @@
   25.13          then have "disjoint_family f"
   25.14            by (auto simp: disjoint_family_on_def f_def)
   25.15          moreover
   25.16 -        have Ai_eq: "A i = (\<Union> x<card C. f x)"
   25.17 +        have Ai_eq: "A i = (\<Union>x<card C. f x)"
   25.18            using f C Ai unfolding bij_betw_def by (simp add: Union_image_eq[symmetric])
   25.19          then have "\<Union>range f = A i"
   25.20            using f C Ai unfolding bij_betw_def by (auto simp: f_def)
    26.1 --- a/src/HOL/Probability/Measure_Space.thy	Fri Jun 26 00:14:10 2015 +0200
    26.2 +++ b/src/HOL/Probability/Measure_Space.thy	Fri Jun 26 10:20:33 2015 +0200
    26.3 @@ -172,17 +172,17 @@
    26.4    case empty thus ?case using f by (auto simp: positive_def)
    26.5  next
    26.6    case (insert x F)
    26.7 -  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+
    26.8 -  have subs: "(\<Union> i\<in>F. A i) - A x \<subseteq> (\<Union> i\<in>F. A i)" by auto
    26.9 -  have "(\<Union> i\<in>(insert x F). A i) = A x \<union> ((\<Union> i\<in>F. A i) - A x)" by auto
   26.10 -  hence "f (\<Union> i\<in>(insert x F). A i) = f (A x \<union> ((\<Union> i\<in>F. A i) - A x))"
   26.11 +  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+
   26.12 +  have subs: "(\<Union>i\<in>F. A i) - A x \<subseteq> (\<Union>i\<in>F. A i)" by auto
   26.13 +  have "(\<Union>i\<in>(insert x F). A i) = A x \<union> ((\<Union>i\<in>F. A i) - A x)" by auto
   26.14 +  hence "f (\<Union>i\<in>(insert x F). A i) = f (A x \<union> ((\<Union>i\<in>F. A i) - A x))"
   26.15      by simp
   26.16 -  also have "\<dots> = f (A x) + f ((\<Union> i\<in>F. A i) - A x)"
   26.17 +  also have "\<dots> = f (A x) + f ((\<Union>i\<in>F. A i) - A x)"
   26.18      using f(2) by (rule additiveD) (insert in_M, auto)
   26.19 -  also have "\<dots> \<le> f (A x) + f (\<Union> i\<in>F. A i)"
   26.20 +  also have "\<dots> \<le> f (A x) + f (\<Union>i\<in>F. A i)"
   26.21      using additive_increasing[OF f] in_M subs by (auto simp: increasing_def intro: add_left_mono)
   26.22    also have "\<dots> \<le> f (A x) + (\<Sum>i\<in>F. f (A i))" using insert by (auto intro: add_left_mono)
   26.23 -  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
   26.24 +  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
   26.25  qed
   26.26  
   26.27  lemma (in ring_of_sets) countably_additive_additive:
   26.28 @@ -292,7 +292,7 @@
   26.29    have *: "(\<Union>n. (\<Union>i<n. A i)) = (\<Union>i. A i)" by auto
   26.30    have "(\<lambda>n. f (\<Union>i<n. A i)) ----> f (\<Union>i. A i)"
   26.31    proof (unfold *[symmetric], intro cont[rule_format])
   26.32 -    show "range (\<lambda>i. \<Union> i<i. A i) \<subseteq> M" "(\<Union>i. \<Union> i<i. A i) \<in> M"
   26.33 +    show "range (\<lambda>i. \<Union>i<i. A i) \<subseteq> M" "(\<Union>i. \<Union>i<i. A i) \<in> M"
   26.34        using A * by auto
   26.35    qed (force intro!: incseq_SucI)
   26.36    moreover have "\<And>n. f (\<Union>i<n. A i) = (\<Sum>i<n. f (A i))"
   26.37 @@ -657,10 +657,10 @@
   26.38  
   26.39  lemma emeasure_UN_eq_0:
   26.40    assumes "\<And>i::nat. emeasure M (N i) = 0" and "range N \<subseteq> sets M"
   26.41 -  shows "emeasure M (\<Union> i. N i) = 0"
   26.42 +  shows "emeasure M (\<Union>i. N i) = 0"
   26.43  proof -
   26.44 -  have "0 \<le> emeasure M (\<Union> i. N i)" using assms by auto
   26.45 -  moreover have "emeasure M (\<Union> i. N i) \<le> 0"
   26.46 +  have "0 \<le> emeasure M (\<Union>i. N i)" using assms by auto
   26.47 +  moreover have "emeasure M (\<Union>i. N i) \<le> 0"
   26.48      using emeasure_subadditive_countably[OF assms(2)] assms(1) by simp
   26.49    ultimately show ?thesis by simp
   26.50  qed
   26.51 @@ -1173,9 +1173,9 @@
   26.52        from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto
   26.53        with F show ?thesis by fastforce
   26.54      qed
   26.55 -    show "emeasure M (\<Union> i\<le>n. F i) \<noteq> \<infinity>" for n
   26.56 +    show "emeasure M (\<Union>i\<le>n. F i) \<noteq> \<infinity>" for n
   26.57      proof -
   26.58 -      have "emeasure M (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. emeasure M (F i))"
   26.59 +      have "emeasure M (\<Union>i\<le>n. F i) \<le> (\<Sum>i\<le>n. emeasure M (F i))"
   26.60          using F by (auto intro!: emeasure_subadditive_finite)
   26.61        also have "\<dots> < \<infinity>"
   26.62          using F by (auto simp: setsum_Pinfty)
   26.63 @@ -1579,12 +1579,12 @@
   26.64    assumes "range f \<subseteq> sets M" "range g \<subseteq> sets M"
   26.65    assumes "disjoint_family f" "disjoint_family g"
   26.66    assumes "\<And> n :: nat. measure M (f n) = measure M (g n)"
   26.67 -  shows "measure M (\<Union> i. f i) = measure M (\<Union> i. g i)"
   26.68 +  shows "measure M (\<Union>i. f i) = measure M (\<Union>i. g i)"
   26.69  using assms
   26.70  proof -
   26.71 -  have a: "(\<lambda> i. measure M (f i)) sums (measure M (\<Union> i. f i))"
   26.72 +  have a: "(\<lambda> i. measure M (f i)) sums (measure M (\<Union>i. f i))"
   26.73      by (rule finite_measure_UNION[OF assms(1,3)])
   26.74 -  have b: "(\<lambda> i. measure M (g i)) sums (measure M (\<Union> i. g i))"
   26.75 +  have b: "(\<lambda> i. measure M (g i)) sums (measure M (\<Union>i. g i))"
   26.76      by (rule finite_measure_UNION[OF assms(2,4)])
   26.77    show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp
   26.78  qed
   26.79 @@ -1592,9 +1592,9 @@
   26.80  lemma (in finite_measure) measure_countably_zero:
   26.81    assumes "range c \<subseteq> sets M"
   26.82    assumes "\<And> i. measure M (c i) = 0"
   26.83 -  shows "measure M (\<Union> i :: nat. c i) = 0"
   26.84 +  shows "measure M (\<Union>i :: nat. c i) = 0"
   26.85  proof (rule antisym)
   26.86 -  show "measure M (\<Union> i :: nat. c i) \<le> 0"
   26.87 +  show "measure M (\<Union>i :: nat. c i) \<le> 0"
   26.88      using finite_measure_subadditive_countably[OF assms(1)] by (simp add: assms(2))
   26.89  qed (simp add: measure_nonneg)
   26.90  
   26.91 @@ -1633,12 +1633,12 @@
   26.92    assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> sets M"
   26.93    assumes "finite s"
   26.94    assumes disjoint: "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}"
   26.95 -  assumes upper: "space M \<subseteq> (\<Union> i \<in> s. f i)"
   26.96 +  assumes upper: "space M \<subseteq> (\<Union>i \<in> s. f i)"
   26.97    shows "measure M e = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
   26.98  proof -
   26.99 -  have e: "e = (\<Union> i \<in> s. e \<inter> f i)"
  26.100 +  have e: "e = (\<Union>i \<in> s. e \<inter> f i)"
  26.101      using `e \<in> sets M` sets.sets_into_space upper by blast
  26.102 -  hence "measure M e = measure M (\<Union> i \<in> s. e \<inter> f i)" by simp
  26.103 +  hence "measure M e = measure M (\<Union>i \<in> s. e \<inter> f i)" by simp
  26.104    also have "\<dots> = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
  26.105    proof (rule finite_measure_finite_Union)
  26.106      show "finite s" by fact
    27.1 --- a/src/HOL/Probability/Projective_Limit.thy	Fri Jun 26 00:14:10 2015 +0200
    27.2 +++ b/src/HOL/Probability/Projective_Limit.thy	Fri Jun 26 10:20:33 2015 +0200
    27.3 @@ -282,15 +282,15 @@
    27.4        have Y_notempty: "\<And>n. n \<ge> 1 \<Longrightarrow> (Y n) \<noteq> {}"
    27.5        proof -
    27.6          fix n::nat assume "n \<ge> 1" hence "Y n \<subseteq> Z n" by fact
    27.7 -        have "Y n = (\<Inter> i\<in>{1..n}. emb I (J n) (emb (J n) (J i) (K i)))" using J J_mono
    27.8 +        have "Y n = (\<Inter>i\<in>{1..n}. emb I (J n) (emb (J n) (J i) (K i)))" using J J_mono
    27.9            by (auto simp: Y_def Z'_def)
   27.10 -        also have "\<dots> = prod_emb I (\<lambda>_. borel) (J n) (\<Inter> i\<in>{1..n}. emb (J n) (J i) (K i))"
   27.11 +        also have "\<dots> = prod_emb I (\<lambda>_. borel) (J n) (\<Inter>i\<in>{1..n}. emb (J n) (J i) (K i))"
   27.12            using `n \<ge> 1`
   27.13            by (subst prod_emb_INT) auto
   27.14          finally
   27.15          have Y_emb:
   27.16            "Y n = prod_emb I (\<lambda>_. borel) (J n)
   27.17 -            (\<Inter> i\<in>{1..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i))" .
   27.18 +            (\<Inter>i\<in>{1..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i))" .
   27.19          hence "Y n \<in> ?G" using J J_mono K_sets `n \<ge> 1` by (intro generatorI[OF _ _ _ _ Y_emb]) auto
   27.20          hence "\<bar>\<mu>G (Y n)\<bar> \<noteq> \<infinity>" unfolding Y_emb using J J_mono K_sets `n \<ge> 1`
   27.21            by (subst mu_G_eq) (auto simp: limP_finite proj_sets mu_G_eq)
   27.22 @@ -317,11 +317,11 @@
   27.23              (auto dest!: bspec[where x=n]
   27.24              simp: extensional_restrict emeasure_eq_measure prod_emb_iff simp del: limP_finite
   27.25              intro!: measure_Diff[symmetric] set_mp[OF K_B])
   27.26 -        also have subs: "Z n - Y n \<subseteq> (\<Union> i\<in>{1..n}. (Z i - Z' i))" using Z' Z `n \<ge> 1`
   27.27 +        also have subs: "Z n - Y n \<subseteq> (\<Union>i\<in>{1..n}. (Z i - Z' i))" using Z' Z `n \<ge> 1`
   27.28            unfolding Y_def by (force simp: decseq_def)
   27.29 -        have "Z n - Y n \<in> ?G" "(\<Union> i\<in>{1..n}. (Z i - Z' i)) \<in> ?G"
   27.30 +        have "Z n - Y n \<in> ?G" "(\<Union>i\<in>{1..n}. (Z i - Z' i)) \<in> ?G"
   27.31            using `Z' _ \<in> ?G` `Z _ \<in> ?G` `Y _ \<in> ?G` by auto
   27.32 -        hence "\<mu>G (Z n - Y n) \<le> \<mu>G (\<Union> i\<in>{1..n}. (Z i - Z' i))"
   27.33 +        hence "\<mu>G (Z n - Y n) \<le> \<mu>G (\<Union>i\<in>{1..n}. (Z i - Z' i))"
   27.34            using subs G.additive_increasing[OF positive_mu_G[OF `I \<noteq> {}`] additive_mu_G[OF `I \<noteq> {}`]]
   27.35            unfolding increasing_def by auto
   27.36          also have "\<dots> \<le> (\<Sum> i\<in>{1..n}. \<mu>G (Z i - Z' i))" using `Z _ \<in> ?G` `Z' _ \<in> ?G`
    28.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Jun 26 00:14:10 2015 +0200
    28.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Fri Jun 26 10:20:33 2015 +0200
    28.3 @@ -625,7 +625,7 @@
    28.4        next
    28.5          case (Suc n)
    28.6          with `?O n \<in> ?Q` `?O (Suc n) \<in> ?Q`
    28.7 -            emeasure_Diff[OF _ _ _ O_mono, of N n] emeasure_nonneg[of N "(\<Union> x\<le>n. Q' x)"]
    28.8 +            emeasure_Diff[OF _ _ _ O_mono, of N n] emeasure_nonneg[of N "(\<Union>x\<le>n. Q' x)"]
    28.9          show ?thesis
   28.10            by (auto simp: sets_eq ereal_minus_eq_PInfty_iff Q_def)
   28.11        qed }
    29.1 --- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Fri Jun 26 00:14:10 2015 +0200
    29.2 +++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Fri Jun 26 10:20:33 2015 +0200
    29.3 @@ -289,12 +289,12 @@
    29.4    have [simp]: "length xs = n" using assms
    29.5      by (auto simp: dc_crypto inversion_def [abs_def])
    29.6  
    29.7 -  have "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union> i < n. ?set i)"
    29.8 +  have "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union>i < n. ?set i)"
    29.9      unfolding dc_crypto payer_def by auto
   29.10 -  also have "\<dots> = (\<Union> ?sets)" by auto
   29.11 -  finally have eq_Union: "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union> ?sets)" by simp
   29.12 +  also have "\<dots> = (\<Union>?sets)" by auto
   29.13 +  finally have eq_Union: "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union>?sets)" by simp
   29.14  
   29.15 -  have card_double: "2 * card ?sets = card (\<Union> ?sets)"
   29.16 +  have card_double: "2 * card ?sets = card (\<Union>?sets)"
   29.17    proof (rule card_partition)
   29.18      show "finite ?sets" by simp
   29.19      { fix i assume "i < n"
    30.1 --- a/src/HOL/Topological_Spaces.thy	Fri Jun 26 00:14:10 2015 +0200
    30.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Jun 26 10:20:33 2015 +0200
    30.3 @@ -20,7 +20,7 @@
    30.4  class topological_space = "open" +
    30.5    assumes open_UNIV [simp, intro]: "open UNIV"
    30.6    assumes open_Int [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)"
    30.7 -  assumes open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union> K)"
    30.8 +  assumes open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union>K)"
    30.9  begin
   30.10  
   30.11  definition
   30.12 @@ -66,7 +66,7 @@
   30.13  lemma closed_INT [continuous_intros, intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)"
   30.14    unfolding closed_def by auto
   30.15  
   30.16 -lemma closed_Inter [continuous_intros, intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)"
   30.17 +lemma closed_Inter [continuous_intros, intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter>K)"
   30.18    unfolding closed_def uminus_Inf by auto
   30.19  
   30.20  lemma closed_Union [continuous_intros, intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
   30.21 @@ -1067,12 +1067,12 @@
   30.22        by (auto simp: decseq_def)
   30.23      show "\<And>n. x \<in> (\<Inter>i\<le>n. A i)" "\<And>n. open (\<Inter>i\<le>n. A i)"
   30.24        using A by auto
   30.25 -    show "nhds x = (INF n. principal (\<Inter> i\<le>n. A i))"
   30.26 +    show "nhds x = (INF n. principal (\<Inter>i\<le>n. A i))"
   30.27        using A unfolding nhds_def
   30.28        apply (intro INF_eq)
   30.29        apply simp_all
   30.30        apply force
   30.31 -      apply (intro exI[of _ "\<Inter> i\<le>n. A i" for n] conjI open_INT)
   30.32 +      apply (intro exI[of _ "\<Inter>i\<le>n. A i" for n] conjI open_INT)
   30.33        apply auto
   30.34        done
   30.35    qed
   30.36 @@ -1521,7 +1521,7 @@
   30.37      "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))"
   30.38  
   30.39  lemma compactI:
   30.40 -  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'"
   30.41 +  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'"
   30.42    shows "compact s"
   30.43    unfolding compact_eq_heine_borel using assms by metis
   30.44  
   30.45 @@ -1584,8 +1584,8 @@
   30.46  qed
   30.47  
   30.48  lemma compact_imp_fip:
   30.49 -  "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>
   30.50 -    s \<inter> (\<Inter> f) \<noteq> {}"
   30.51 +  "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>
   30.52 +    s \<inter> (\<Inter>f) \<noteq> {}"
   30.53    unfolding compact_fip by auto
   30.54  
   30.55  lemma compact_imp_fip_image:
    31.1 --- a/src/HOL/ZF/Games.thy	Fri Jun 26 00:14:10 2015 +0200
    31.2 +++ b/src/HOL/ZF/Games.thy	Fri Jun 26 10:20:33 2015 +0200
    31.3 @@ -831,10 +831,10 @@
    31.4    Pg_less_def: "G < H \<longleftrightarrow> G \<le> H \<and> G \<noteq> (H::Pg)"
    31.5  
    31.6  definition
    31.7 -  Pg_minus_def: "- G = the_elem (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
    31.8 +  Pg_minus_def: "- G = the_elem (\<Union>g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
    31.9  
   31.10  definition
   31.11 -  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})})"
   31.12 +  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})})"
   31.13  
   31.14  definition
   31.15    Pg_diff_def: "G - H = G + (- (H::Pg))"