diff -r 5e5e6ad3922c -r e6f291cb5810 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Sat Aug 27 17:26:14 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Sun Aug 28 09:20:12 2011 -0700
@@ -2191,9 +2191,9 @@
   have 3: "\<And>x n. 0 \<le> f n x - f 0 x" using `mono f`
       unfolding mono_def le_fun_def by (auto simp: field_simps)
   have 4: "\<And>x. (\<lambda>i. f i x - f 0 x) ----> u x - f 0 x"
-    using lim by (auto intro!: LIMSEQ_diff)
+    using lim by (auto intro!: tendsto_diff)
   have 5: "(\<lambda>i. (\<integral>x. f i x - f 0 x \<partial>M)) ----> x - integral\<^isup>L M (f 0)"
-    using f ilim by (auto intro!: LIMSEQ_diff simp: integral_diff)
+    using f ilim by (auto intro!: tendsto_diff simp: integral_diff)
   note diff = integral_monotone_convergence_pos[OF 1 2 3 4 5]
   have "integrable M (\<lambda>x. (u x - f 0 x) + f 0 x)"
     using diff(1) f by (rule integral_add(1))
@@ -2329,7 +2329,7 @@
   and "(\<lambda>i. integral\<^isup>L M (u i)) ----> integral\<^isup>L M u'" (is ?lim)
 proof -
   { fix x j assume x: "x \<in> space M"
-    from u'[OF x] have "(\<lambda>i. \<bar>u i x\<bar>) ----> \<bar>u' x\<bar>" by (rule LIMSEQ_imp_rabs)
+    from u'[OF x] have "(\<lambda>i. \<bar>u i x\<bar>) ----> \<bar>u' x\<bar>" by (rule tendsto_rabs)
     from LIMSEQ_le_const2[OF this]
     have "\<bar>u' x\<bar> \<le> w x" using bound[OF x] by auto }
   note u'_bound = this
@@ -2400,7 +2400,7 @@
         unfolding ereal_max_0
       proof (rule lim_imp_Liminf[symmetric], unfold lim_ereal)
         have "(\<lambda>i. ?diff i x) ----> 2 * w x - \<bar>u' x - u' x\<bar>"
-          using u'[OF x] by (safe intro!: LIMSEQ_diff LIMSEQ_const LIMSEQ_imp_rabs)
+          using u'[OF x] by (safe intro!: tendsto_intros)
         then show "(\<lambda>i. max 0 (?diff i x)) ----> max 0 (2 * w x)"
           by (auto intro!: tendsto_real_max simp add: lim_ereal)
       qed (rule trivial_limit_sequentially)
@@ -2492,7 +2492,7 @@
     show "mono ?w'"
       by (auto simp: mono_def le_fun_def intro!: setsum_mono2)
     { fix x show "(\<lambda>n. ?w' n x) ----> ?w x"
-        using w by (cases "x \<in> space M") (simp_all add: LIMSEQ_const sums_def) }
+        using w by (cases "x \<in> space M") (simp_all add: tendsto_const sums_def) }
     have *: "\<And>n. integral\<^isup>L M (?w' n) = (\<Sum>i = 0..< n. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
       using borel by (simp add: integral_setsum integrable_abs cong: integral_cong)
     from abs_sum