--- a/src/HOL/Library/BigO.thy Wed Apr 22 12:15:27 2015 +0200
+++ b/src/HOL/Library/BigO.thy Wed Apr 22 13:48:34 2015 +0200
@@ -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 Wed Apr 22 12:15:27 2015 +0200
+++ b/src/HOL/Probability/Measure_Space.thy Wed Apr 22 13:48:34 2015 +0200
@@ -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