diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Probability/Regularity.thy
--- a/src/HOL/Probability/Regularity.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Probability/Regularity.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -144,7 +144,7 @@
   } note M_space = this
   {
     fix e ::real and n :: nat assume "e > 0" "n > 0"
-    hence "1/n > 0" "e * 2 powr - n > 0" by (auto intro: mult_pos_pos)
+    hence "1/n > 0" "e * 2 powr - n > 0" by (auto)
     from M_space[OF `1/n>0`]
     have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) ----> measure M (space M)"
       unfolding emeasure_eq_measure by simp
@@ -271,7 +271,7 @@
         show "?G (1 / real (Suc i)) \<in> sets M" by (simp add: sb borel_open)
       next
         show "decseq (\<lambda>i. {x. infdist x A < 1 / real (Suc i)})"
-          by (auto intro: less_trans intro!: divide_strict_left_mono mult_pos_pos
+          by (auto intro: less_trans intro!: divide_strict_left_mono
             simp: decseq_def le_eq_less_or_eq)
       qed simp
       finally