summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Probability/Regularity.thy

changeset 52141 | eff000cab70f |

parent 51000 | c9adb50f74ad |

child 56166 | 9a241bc276cd |

--- a/src/HOL/Probability/Regularity.thy Sat May 25 15:44:08 2013 +0200 +++ b/src/HOL/Probability/Regularity.thy Sat May 25 15:44:29 2013 +0200 @@ -209,8 +209,8 @@ from nat_approx_posE[OF this] guess n . note n = this let ?k = "from_nat_into X ` {0..k e (Suc n)}" have "finite ?k" by simp - moreover have "K \<subseteq> \<Union>(\<lambda>x. ball x e') ` ?k" unfolding K_def B_def using n by force - ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>(\<lambda>x. ball x e') ` k" by blast + moreover have "K \<subseteq> \<Union>((\<lambda>x. ball x e') ` ?k)" unfolding K_def B_def using n by force + ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>((\<lambda>x. ball x e') ` k)" by blast qed ultimately show "?thesis e " by (auto simp: sU)