src/HOL/Probability/Regularity.thy
changeset 60017 b785d6d06430
parent 59452 2538b2c51769
child 60636 ee18efe9b246
     1.1 --- a/src/HOL/Probability/Regularity.thy	Thu Apr 09 20:42:38 2015 +0200
     1.2 +++ b/src/HOL/Probability/Regularity.thy	Sat Apr 11 11:56:40 2015 +0100
     1.3 @@ -363,7 +363,7 @@
     1.4        fix e::real assume "e > 0"
     1.5        with measure_LIMSEQ
     1.6        have "\<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>i<n. measure M (D i)) -measure M (\<Union>x. D x)\<bar> < e/2"
     1.7 -        by (auto simp: LIMSEQ_def dist_real_def simp del: less_divide_eq_numeral1)
     1.8 +        by (auto simp: lim_sequentially dist_real_def simp del: less_divide_eq_numeral1)
     1.9        hence "\<exists>n0. \<bar>(\<Sum>i<n0. measure M (D i)) - measure M (\<Union>x. D x)\<bar> < e/2" by auto
    1.10        then obtain n0 where n0: "\<bar>(\<Sum>i<n0. measure M (D i)) - measure M (\<Union>i. D i)\<bar> < e/2"
    1.11          unfolding choice_iff by blast