src/HOL/Probability/Regularity.thy
changeset 56544 b60d5d119489
parent 56541 0e3abadbef39
child 58184 db1381d811ab
     1.1 --- a/src/HOL/Probability/Regularity.thy	Fri Apr 11 23:22:00 2014 +0200
     1.2 +++ b/src/HOL/Probability/Regularity.thy	Sat Apr 12 17:26:27 2014 +0200
     1.3 @@ -144,7 +144,7 @@
     1.4    } note M_space = this
     1.5    {
     1.6      fix e ::real and n :: nat assume "e > 0" "n > 0"
     1.7 -    hence "1/n > 0" "e * 2 powr - n > 0" by (auto intro: mult_pos_pos)
     1.8 +    hence "1/n > 0" "e * 2 powr - n > 0" by (auto)
     1.9      from M_space[OF `1/n>0`]
    1.10      have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) ----> measure M (space M)"
    1.11        unfolding emeasure_eq_measure by simp
    1.12 @@ -271,7 +271,7 @@
    1.13          show "?G (1 / real (Suc i)) \<in> sets M" by (simp add: sb borel_open)
    1.14        next
    1.15          show "decseq (\<lambda>i. {x. infdist x A < 1 / real (Suc i)})"
    1.16 -          by (auto intro: less_trans intro!: divide_strict_left_mono mult_pos_pos
    1.17 +          by (auto intro: less_trans intro!: divide_strict_left_mono
    1.18              simp: decseq_def le_eq_less_or_eq)
    1.19        qed simp
    1.20        finally