--- a/src/HOL/Probability/Caratheodory.thy Sat Aug 27 17:26:14 2011 +0200
+++ b/src/HOL/Probability/Caratheodory.thy Sun Aug 28 09:20:12 2011 -0700
@@ -128,7 +128,7 @@
by (induct n) (auto simp add: binaryset_def f)
qed
moreover
- have "... ----> f A + f B" by (rule LIMSEQ_const)
+ have "... ----> f A + f B" by (rule tendsto_const)
ultimately
have "(\<lambda>n. \<Sum>i< Suc (Suc n). f (binaryset A B i)) ----> f A + f B"
by metis
@@ -985,7 +985,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 LIMSEQ_diff_approach_zero2[OF LIMSEQ_const])
+ by (rule LIMSEQ_diff_approach_zero2[OF tendsto_const])
then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
using A by (subst (1 2) f') auto
qed