src/HOL/Probability/Measure_Space.thy
changeset 60141 833adf7db7d8
parent 60063 81835db730e8
child 60142 3275dddf356f
     1.1 --- a/src/HOL/Probability/Measure_Space.thy	Mon Apr 20 13:46:36 2015 +0100
     1.2 +++ b/src/HOL/Probability/Measure_Space.thy	Tue Apr 21 17:19:00 2015 +0100
     1.3 @@ -389,7 +389,7 @@
     1.4    ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) ----> 0"
     1.5      by (simp add: zero_ereal_def)
     1.6    then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
     1.7 -    by (rule LIMSEQ_diff_approach_zero2[OF tendsto_const])
     1.8 +    by (rule Lim_transform[OF tendsto_const])
     1.9    then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
    1.10      using A by (subst (1 2) f') auto
    1.11  qed