src/HOL/Probability/Regularity.thy
 changeset 58184 db1381d811ab parent 56544 b60d5d119489 child 58876 1888e3cb8048
```     1.1 --- a/src/HOL/Probability/Regularity.thy	Thu Sep 04 11:53:39 2014 +0200
1.2 +++ b/src/HOL/Probability/Regularity.thy	Thu Sep 04 14:02:37 2014 +0200
1.3 @@ -163,7 +163,7 @@
1.4      by blast
1.5    then obtain k where k: "\<forall>e\<in>{0<..}. \<forall>n\<in>{0<..}. measure M (space M) - e * 2 powr - real (n::nat)
1.6      \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"
1.7 -    apply atomize_elim unfolding bchoice_iff .
1.8 +    by metis
1.9    hence k: "\<And>e n. e > 0 \<Longrightarrow> n > 0 \<Longrightarrow> measure M (space M) - e * 2 powr - n
1.10      \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"
1.11      unfolding Ball_def by blast
1.12 @@ -209,8 +209,8 @@
1.13        from nat_approx_posE[OF this] guess n . note n = this
1.14        let ?k = "from_nat_into X ` {0..k e (Suc n)}"
1.15        have "finite ?k" by simp
1.16 -      moreover have "K \<subseteq> \<Union>((\<lambda>x. ball x e') ` ?k)" unfolding K_def B_def using n by force
1.17 -      ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>((\<lambda>x. ball x e') ` k)" by blast
1.18 +      moreover have "K \<subseteq> (\<Union>x\<in>?k. ball x e')" unfolding K_def B_def using n by force
1.19 +      ultimately show "\<exists>k. finite k \<and> K \<subseteq> (\<Union>x\<in>k. ball x e')" by blast
1.20      qed
1.21      ultimately
1.22      show "?thesis e " by (auto simp: sU)
```