fixes for limits
authorpaulson <lp15@cam.ac.uk>
Wed, 22 Apr 2015 12:43:06 +0100
changeset 60142 3275dddf356f
parent 60141 833adf7db7d8
child 60145 123ac30760df
fixes for limits
src/HOL/Library/BigO.thy
src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Library/BigO.thy	Tue Apr 21 17:19:00 2015 +0100
+++ b/src/HOL/Library/BigO.thy	Wed Apr 22 12:43:06 2015 +0100
@@ -870,7 +870,7 @@
   apply (drule bigo_LIMSEQ1)
   apply assumption
   apply (simp only: fun_diff_def)
-  apply (erule Lim_transform)
+  apply (erule Lim_transform2)
   apply assumption
   done
 
--- a/src/HOL/Probability/Measure_Space.thy	Tue Apr 21 17:19:00 2015 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Wed Apr 22 12:43:06 2015 +0100
@@ -389,7 +389,7 @@
   ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) ----> 0"
     by (simp add: zero_ereal_def)
   then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
-    by (rule Lim_transform[OF tendsto_const])
+    by (rule Lim_transform2[OF tendsto_const])
   then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
     using A by (subst (1 2) f') auto
 qed