diff -r 1fd920a86173 -r 0e3abadbef39 src/HOL/Probability/Regularity.thy
--- a/src/HOL/Probability/Regularity.thy	Fri Apr 11 17:53:16 2014 +0200
+++ b/src/HOL/Probability/Regularity.thy	Fri Apr 11 22:53:33 2014 +0200
@@ -377,7 +377,7 @@
       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)"
       proof
         fix i
-        from `0 < e` have "0 < e/(2*Suc n0)" by (auto intro: divide_pos_pos)
+        from `0 < e` have "0 < e/(2*Suc n0)" by simp
         have "emeasure M (D i) = (SUP K:{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)"
           using union by blast
         from SUP_approx_ereal[OF `0 < e/(2*Suc n0)` this]
@@ -418,7 +418,7 @@
       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)"
       proof
         fix i::nat
-        from `0 < e` have "0 < e/(2 powr Suc i)" by (auto intro: divide_pos_pos)
+        from `0 < e` have "0 < e/(2 powr Suc i)" by simp
         have "emeasure M (D i) = (INF U:{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)"
           using union by blast
         from INF_approx_ereal[OF `0 < e/(2 powr Suc i)` this]