fixes for limits
authorpaulson <lp15@cam.ac.uk>
Wed Apr 22 12:43:06 2015 +0100 (2015-04-22)
changeset 601423275dddf356f
parent 60141 833adf7db7d8
child 60145 123ac30760df
fixes for limits
src/HOL/Library/BigO.thy
src/HOL/Probability/Measure_Space.thy
     1.1 --- a/src/HOL/Library/BigO.thy	Tue Apr 21 17:19:00 2015 +0100
     1.2 +++ b/src/HOL/Library/BigO.thy	Wed Apr 22 12:43:06 2015 +0100
     1.3 @@ -870,7 +870,7 @@
     1.4    apply (drule bigo_LIMSEQ1)
     1.5    apply assumption
     1.6    apply (simp only: fun_diff_def)
     1.7 -  apply (erule Lim_transform)
     1.8 +  apply (erule Lim_transform2)
     1.9    apply assumption
    1.10    done
    1.11  
     2.1 --- a/src/HOL/Probability/Measure_Space.thy	Tue Apr 21 17:19:00 2015 +0100
     2.2 +++ b/src/HOL/Probability/Measure_Space.thy	Wed Apr 22 12:43:06 2015 +0100
     2.3 @@ -389,7 +389,7 @@
     2.4    ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) ----> 0"
     2.5      by (simp add: zero_ereal_def)
     2.6    then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
     2.7 -    by (rule Lim_transform[OF tendsto_const])
     2.8 +    by (rule Lim_transform2[OF tendsto_const])
     2.9    then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
    2.10      using A by (subst (1 2) f') auto
    2.11  qed