# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1429702986 -3600
# Node ID 3275dddf356f51a2fc46d8860a3df6220d56458d
# Parent  833adf7db7d83429100ef31fd667912a570c4c55
fixes for limits

diff -r 833adf7db7d8 -r 3275dddf356f src/HOL/Library/BigO.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
 
diff -r 833adf7db7d8 -r 3275dddf356f src/HOL/Probability/Measure_Space.thy
--- 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