src/HOL/Probability/Regularity.thy
 changeset 56541 0e3abadbef39 parent 56212 3253aaf73a01 child 56544 b60d5d119489
```     1.1 --- a/src/HOL/Probability/Regularity.thy	Fri Apr 11 17:53:16 2014 +0200
1.2 +++ b/src/HOL/Probability/Regularity.thy	Fri Apr 11 22:53:33 2014 +0200
1.3 @@ -377,7 +377,7 @@
1.4        have "\<forall>i. \<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)"
1.5        proof
1.6          fix i
1.7 -        from `0 < e` have "0 < e/(2*Suc n0)" by (auto intro: divide_pos_pos)
1.8 +        from `0 < e` have "0 < e/(2*Suc n0)" by simp
1.9          have "emeasure M (D i) = (SUP K:{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)"
1.10            using union by blast
1.11          from SUP_approx_ereal[OF `0 < e/(2*Suc n0)` this]
1.12 @@ -418,7 +418,7 @@
1.13        have "\<forall>i::nat. \<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
1.14        proof
1.15          fix i::nat
1.16 -        from `0 < e` have "0 < e/(2 powr Suc i)" by (auto intro: divide_pos_pos)
1.17 +        from `0 < e` have "0 < e/(2 powr Suc i)" by simp
1.18          have "emeasure M (D i) = (INF U:{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)"
1.19            using union by blast
1.20          from INF_approx_ereal[OF `0 < e/(2 powr Suc i)` this]
```