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]