discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
authorhuffman
Sun Aug 28 09:20:12 2011 -0700 (2011-08-28)
changeset 44568e6f291cb5810
parent 44549 5e5e6ad3922c
child 44569 44525dd281d4
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
NEWS
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Deriv.thy
src/HOL/Library/FrechetDeriv.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Lim.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NSA/HSEQ.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/SEQ.thy
src/HOL/Series.thy
src/HOL/Transcendental.thy
     1.1 --- a/NEWS	Sat Aug 27 17:26:14 2011 +0200
     1.2 +++ b/NEWS	Sun Aug 28 09:20:12 2011 -0700
     1.3 @@ -246,8 +246,8 @@
     1.4    mult_right.setsum ~> setsum_right_distrib
     1.5    mult_left.diff ~> left_diff_distrib
     1.6  
     1.7 -* Complex_Main: Several redundant theorems about real numbers have
     1.8 -been removed or generalized and renamed. INCOMPATIBILITY.
     1.9 +* Complex_Main: Several redundant theorems have been removed or
    1.10 +replaced by more general versions. INCOMPATIBILITY.
    1.11  
    1.12    real_0_le_divide_iff ~> zero_le_divide_iff
    1.13    realpow_two_disj ~> power2_eq_iff
    1.14 @@ -255,6 +255,53 @@
    1.15    realpow_two_diff ~> square_diff_square_factored
    1.16    exp_ln_eq ~> ln_unique
    1.17    lemma_DERIV_subst ~> DERIV_cong
    1.18 +  LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff
    1.19 +  LIMSEQ_const ~> tendsto_const
    1.20 +  LIMSEQ_norm ~> tendsto_norm
    1.21 +  LIMSEQ_add ~> tendsto_add
    1.22 +  LIMSEQ_minus ~> tendsto_minus
    1.23 +  LIMSEQ_minus_cancel ~> tendsto_minus_cancel
    1.24 +  LIMSEQ_diff ~> tendsto_diff
    1.25 +  bounded_linear.LIMSEQ ~> bounded_linear.tendsto
    1.26 +  bounded_bilinear.LIMSEQ ~> bounded_bilinear.tendsto
    1.27 +  LIMSEQ_mult ~> tendsto_mult
    1.28 +  LIMSEQ_inverse ~> tendsto_inverse
    1.29 +  LIMSEQ_divide ~> tendsto_divide
    1.30 +  LIMSEQ_pow ~> tendsto_power
    1.31 +  LIMSEQ_setsum ~> tendsto_setsum
    1.32 +  LIMSEQ_setprod ~> tendsto_setprod
    1.33 +  LIMSEQ_norm_zero ~> tendsto_norm_zero_iff
    1.34 +  LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff
    1.35 +  LIMSEQ_imp_rabs ~> tendsto_rabs
    1.36 +  LIM_ident ~> tendsto_ident_at
    1.37 +  LIM_const ~> tendsto_const
    1.38 +  LIM_add ~> tendsto_add
    1.39 +  LIM_add_zero ~> tendsto_add_zero
    1.40 +  LIM_minus ~> tendsto_minus
    1.41 +  LIM_diff ~> tendsto_diff
    1.42 +  LIM_norm ~> tendsto_norm
    1.43 +  LIM_norm_zero ~> tendsto_norm_zero
    1.44 +  LIM_norm_zero_cancel ~> tendsto_norm_zero_cancel
    1.45 +  LIM_norm_zero_iff ~> tendsto_norm_zero_iff
    1.46 +  LIM_rabs ~> tendsto_rabs
    1.47 +  LIM_rabs_zero ~> tendsto_rabs_zero
    1.48 +  LIM_rabs_zero_cancel ~> tendsto_rabs_zero_cancel
    1.49 +  LIM_rabs_zero_iff ~> tendsto_rabs_zero_iff
    1.50 +  LIM_compose ~> tendsto_compose
    1.51 +  LIM_mult ~> tendsto_mult
    1.52 +  LIM_scaleR ~> tendsto_scaleR
    1.53 +  LIM_of_real ~> tendsto_of_real
    1.54 +  LIM_power ~> tendsto_power
    1.55 +  LIM_inverse ~> tendsto_inverse
    1.56 +  LIM_sgn ~> tendsto_sgn
    1.57 +  isCont_LIM_compose ~> isCont_tendsto_compose
    1.58 +  bounded_linear.LIM ~> bounded_linear.tendsto
    1.59 +  bounded_linear.LIM_zero ~> bounded_linear.tendsto_zero
    1.60 +  bounded_bilinear.LIM ~> bounded_bilinear.tendsto
    1.61 +  bounded_bilinear.LIM_prod_zero ~> bounded_bilinear.tendsto_zero
    1.62 +  bounded_bilinear.LIM_left_zero ~> bounded_bilinear.tendsto_left_zero
    1.63 +  bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero
    1.64 +  LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at]
    1.65  
    1.66  
    1.67  *** Document preparation ***
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Sat Aug 27 17:26:14 2011 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Aug 28 09:20:12 2011 -0700
     2.3 @@ -1687,7 +1687,7 @@
     2.4  
     2.5    have "norm x < 1" using assms by auto
     2.6    have "?a ----> 0" unfolding Suc_eq_plus1[symmetric] inverse_eq_divide[symmetric]
     2.7 -    using LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_Suc[OF LIMSEQ_power_zero[OF `norm x < 1`]]] by auto
     2.8 +    using tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_Suc[OF LIMSEQ_power_zero[OF `norm x < 1`]]] by auto
     2.9    { fix n have "0 \<le> ?a n" by (rule mult_nonneg_nonneg, auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`) }
    2.10    { fix n have "?a (Suc n) \<le> ?a n" unfolding inverse_eq_divide[symmetric]
    2.11      proof (rule mult_mono)
     3.1 --- a/src/HOL/Deriv.thy	Sat Aug 27 17:26:14 2011 +0200
     3.2 +++ b/src/HOL/Deriv.thy	Sun Aug 28 09:20:12 2011 -0700
     3.3 @@ -37,18 +37,18 @@
     3.4  by (simp add: deriv_def)
     3.5  
     3.6  lemma DERIV_const [simp]: "DERIV (\<lambda>x. k) x :> 0"
     3.7 -by (simp add: deriv_def)
     3.8 +  by (simp add: deriv_def tendsto_const)
     3.9  
    3.10  lemma DERIV_ident [simp]: "DERIV (\<lambda>x. x) x :> 1"
    3.11 -by (simp add: deriv_def cong: LIM_cong)
    3.12 +  by (simp add: deriv_def tendsto_const cong: LIM_cong)
    3.13  
    3.14  lemma DERIV_add:
    3.15    "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x + g x) x :> D + E"
    3.16 -by (simp only: deriv_def add_diff_add add_divide_distrib LIM_add)
    3.17 +  by (simp only: deriv_def add_diff_add add_divide_distrib tendsto_add)
    3.18  
    3.19  lemma DERIV_minus:
    3.20    "DERIV f x :> D \<Longrightarrow> DERIV (\<lambda>x. - f x) x :> - D"
    3.21 -by (simp only: deriv_def minus_diff_minus divide_minus_left LIM_minus)
    3.22 +  by (simp only: deriv_def minus_diff_minus divide_minus_left tendsto_minus)
    3.23  
    3.24  lemma DERIV_diff:
    3.25    "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x - g x) x :> D - E"
    3.26 @@ -64,7 +64,7 @@
    3.27    hence "(\<lambda>h. (f(x+h) - f(x)) / h) -- 0 --> D"
    3.28      by (rule DERIV_D)
    3.29    hence "(\<lambda>h. (f(x+h) - f(x)) / h * h) -- 0 --> D * 0"
    3.30 -    by (intro LIM_mult LIM_ident)
    3.31 +    by (intro tendsto_mult tendsto_ident_at)
    3.32    hence "(\<lambda>h. (f(x+h) - f(x)) * (h / h)) -- 0 --> 0"
    3.33      by simp
    3.34    hence "(\<lambda>h. f(x+h) - f(x)) -- 0 --> 0"
    3.35 @@ -90,7 +90,7 @@
    3.36    hence "(\<lambda>h. f(x+h) * ((g(x+h) - g x) / h) +
    3.37                ((f(x+h) - f x) / h) * g x)
    3.38            -- 0 --> f x * E + D * g x"
    3.39 -    by (intro LIM_add LIM_mult LIM_const DERIV_D f g)
    3.40 +    by (intro tendsto_intros DERIV_D f g)
    3.41    thus "(\<lambda>h. (f(x+h) * g(x+h) - f x * g x) / h)
    3.42           -- 0 --> f x * E + D * g x"
    3.43      by (simp only: DERIV_mult_lemma)
    3.44 @@ -172,7 +172,7 @@
    3.45        by (unfold DERIV_iff2)
    3.46      thus "(\<lambda>z. - (inverse (f z) * ((f z - f x) / (z - x)) * inverse (f x)))
    3.47            -- x --> ?E"
    3.48 -      by (intro LIM_mult LIM_inverse LIM_minus LIM_const lim_f neq)
    3.49 +      by (intro tendsto_intros lim_f neq)
    3.50    qed
    3.51  qed
    3.52  
    3.53 @@ -245,10 +245,10 @@
    3.54    from f have "f -- x --> f x"
    3.55      by (rule DERIV_isCont [unfolded isCont_def])
    3.56    with cont_d have "(\<lambda>z. d (f z)) -- x --> d (f x)"
    3.57 -    by (rule isCont_LIM_compose)
    3.58 +    by (rule isCont_tendsto_compose)
    3.59    hence "(\<lambda>z. d (f z) * ((f z - f x) / (z - x)))
    3.60            -- x --> d (f x) * D"
    3.61 -    by (rule LIM_mult [OF _ f [unfolded DERIV_iff2]])
    3.62 +    by (rule tendsto_mult [OF _ f [unfolded DERIV_iff2]])
    3.63    thus "(\<lambda>z. (g (f z) - g (f x)) / (z - x)) -- x --> E * D"
    3.64      by (simp add: d dfx)
    3.65  qed
    3.66 @@ -485,7 +485,7 @@
    3.67  lemma lim_uminus:
    3.68    fixes g :: "nat \<Rightarrow> 'a::real_normed_vector"
    3.69    shows "convergent g ==> lim (%x. - g x) = - (lim g)"
    3.70 -apply (rule LIMSEQ_minus [THEN limI])
    3.71 +apply (rule tendsto_minus [THEN limI])
    3.72  apply (simp add: convergent_LIMSEQ_iff)
    3.73  done
    3.74  
    3.75 @@ -521,7 +521,7 @@
    3.76                  ((\<forall>n. l \<le> g(n)) & g ----> l)"
    3.77  apply (drule lemma_nest, auto)
    3.78  apply (subgoal_tac "l = m")
    3.79 -apply (drule_tac [2] f = f in LIMSEQ_diff)
    3.80 +apply (drule_tac [2] f = f in tendsto_diff)
    3.81  apply (auto intro: LIMSEQ_unique)
    3.82  done
    3.83  
    3.84 @@ -599,7 +599,7 @@
    3.85           a \<le> b |]
    3.86        ==> P(a,b)"
    3.87  apply (rule Bolzano_nest_unique [where P1=P, THEN exE], assumption+)
    3.88 -apply (rule LIMSEQ_minus_cancel)
    3.89 +apply (rule tendsto_minus_cancel)
    3.90  apply (simp (no_asm_simp) add: Bolzano_bisect_diff LIMSEQ_divide_realpow_zero)
    3.91  apply (rule ccontr)
    3.92  apply (drule not_P_Bolzano_bisect', assumption+)
    3.93 @@ -1488,7 +1488,7 @@
    3.94      using cont 1 2 by (rule isCont_LIM_compose2)
    3.95    thus "(\<lambda>y. inverse ((f (g y) - x) / (g y - g x)))
    3.96          -- x --> inverse D"
    3.97 -    using neq by (rule LIM_inverse)
    3.98 +    using neq by (rule tendsto_inverse)
    3.99  qed
   3.100  
   3.101  
     4.1 --- a/src/HOL/Library/FrechetDeriv.thy	Sat Aug 27 17:26:14 2011 +0200
     4.2 +++ b/src/HOL/Library/FrechetDeriv.thy	Sun Aug 28 09:20:12 2011 -0700
     4.3 @@ -32,13 +32,13 @@
     4.4    by (rule bounded_linear_intro [where K=0], simp_all)
     4.5  
     4.6  lemma FDERIV_const: "FDERIV (\<lambda>x. k) x :> (\<lambda>h. 0)"
     4.7 -  by (simp add: fderiv_def bounded_linear_zero)
     4.8 +  by (simp add: fderiv_def bounded_linear_zero tendsto_const)
     4.9  
    4.10  lemma bounded_linear_ident: "bounded_linear (\<lambda>x. x)"
    4.11    by (rule bounded_linear_intro [where K=1], simp_all)
    4.12  
    4.13  lemma FDERIV_ident: "FDERIV (\<lambda>x. x) x :> (\<lambda>h. h)"
    4.14 -  by (simp add: fderiv_def bounded_linear_ident)
    4.15 +  by (simp add: fderiv_def bounded_linear_ident tendsto_const)
    4.16  
    4.17  subsection {* Addition *}
    4.18  
    4.19 @@ -90,7 +90,7 @@
    4.20    from f' g'
    4.21    have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h
    4.22             + norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0"
    4.23 -    by (rule LIM_add_zero)
    4.24 +    by (rule tendsto_add_zero)
    4.25    thus "(\<lambda>h. norm (f (x + h) + g (x + h) - (f x + g x) - (F h + G h))
    4.26             / norm h) -- 0 --> 0"
    4.27      apply (rule real_LIM_sandwich_zero)
    4.28 @@ -178,13 +178,13 @@
    4.29    have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
    4.30      by (rule FDERIV_D [OF f])
    4.31    hence "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0"
    4.32 -    by (intro LIM_mult_zero LIM_norm_zero LIM_ident)
    4.33 +    by (intro tendsto_mult_zero tendsto_norm_zero tendsto_ident_at)
    4.34    hence "(\<lambda>h. norm (f (x + h) - f x - F h)) -- 0 --> 0"
    4.35      by (simp cong: LIM_cong)
    4.36    hence "(\<lambda>h. f (x + h) - f x - F h) -- 0 --> 0"
    4.37 -    by (rule LIM_norm_zero_cancel)
    4.38 +    by (rule tendsto_norm_zero_cancel)
    4.39    hence "(\<lambda>h. f (x + h) - f x - F h + F h) -- 0 --> 0"
    4.40 -    by (intro LIM_add_zero F.LIM_zero LIM_ident)
    4.41 +    by (intro tendsto_add_zero F.tendsto_zero tendsto_ident_at)
    4.42    hence "(\<lambda>h. f (x + h) - f x) -- 0 --> 0"
    4.43      by simp
    4.44    thus "isCont f x"
    4.45 @@ -266,11 +266,11 @@
    4.46        apply (rule FDERIV_isCont [OF f])
    4.47        done
    4.48      have Ng: "?Ng -- 0 --> 0"
    4.49 -      using isCont_LIM_compose [OF Ng1 Ng2] by simp
    4.50 +      using isCont_tendsto_compose [OF Ng1 Ng2] by simp
    4.51  
    4.52      have "(\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF))
    4.53             -- 0 --> 0 * kG + 0 * (0 + kF)"
    4.54 -      by (intro LIM_add LIM_mult LIM_const Nf Ng)
    4.55 +      by (intro tendsto_intros Nf Ng)
    4.56      thus "(\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)) -- 0 --> 0"
    4.57        by simp
    4.58    next
    4.59 @@ -369,7 +369,7 @@
    4.60      from f g isCont_iff [THEN iffD1, OF FDERIV_isCont [OF g]]
    4.61      have "?fun2 -- 0 -->
    4.62            norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K"
    4.63 -      by (intro LIM_add LIM_mult LIM_const LIM_norm LIM_zero FDERIV_D)
    4.64 +      by (intro tendsto_intros LIM_zero FDERIV_D)
    4.65      thus "?fun2 -- 0 --> 0"
    4.66        by simp
    4.67    next
    4.68 @@ -474,12 +474,12 @@
    4.69      proof (rule real_LIM_sandwich_zero)
    4.70        show "(\<lambda>h. norm (?inv (x + h) - ?inv x) * norm (?inv x))
    4.71              -- 0 --> 0"
    4.72 -        apply (rule LIM_mult_left_zero)
    4.73 -        apply (rule LIM_norm_zero)
    4.74 +        apply (rule tendsto_mult_left_zero)
    4.75 +        apply (rule tendsto_norm_zero)
    4.76          apply (rule LIM_zero)
    4.77          apply (rule LIM_offset_zero)
    4.78 -        apply (rule LIM_inverse)
    4.79 -        apply (rule LIM_ident)
    4.80 +        apply (rule tendsto_inverse)
    4.81 +        apply (rule tendsto_ident_at)
    4.82          apply (rule x)
    4.83          done
    4.84      next
    4.85 @@ -517,7 +517,7 @@
    4.86   apply (subst diff_divide_distrib)
    4.87   apply (subst times_divide_eq_left [symmetric])
    4.88   apply (simp cong: LIM_cong)
    4.89 - apply (simp add: LIM_norm_zero_iff LIM_zero_iff)
    4.90 + apply (simp add: tendsto_norm_zero_iff LIM_zero_iff)
    4.91  done
    4.92  
    4.93  end
     5.1 --- a/src/HOL/Library/Product_Vector.thy	Sat Aug 27 17:26:14 2011 +0200
     5.2 +++ b/src/HOL/Library/Product_Vector.thy	Sun Aug 28 09:20:12 2011 -0700
     5.3 @@ -544,7 +544,7 @@
     5.4  apply (rule FDERIV_bounded_linear [OF g])
     5.5  apply (simp add: norm_Pair)
     5.6  apply (rule real_LIM_sandwich_zero)
     5.7 -apply (rule LIM_add_zero)
     5.8 +apply (rule tendsto_add_zero)
     5.9  apply (rule FDERIV_D [OF f])
    5.10  apply (rule FDERIV_D [OF g])
    5.11  apply (rename_tac h)
     6.1 --- a/src/HOL/Lim.thy	Sat Aug 27 17:26:14 2011 +0200
     6.2 +++ b/src/HOL/Lim.thy	Sun Aug 28 09:20:12 2011 -0700
     6.3 @@ -211,51 +211,6 @@
     6.4    finally show "norm (g x - 0) \<le> norm (f x - 0)" .
     6.5  qed
     6.6  
     6.7 -text {* Bounded Linear Operators *}
     6.8 -
     6.9 -lemma (in bounded_linear) LIM:
    6.10 -  "g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
    6.11 -by (rule tendsto)
    6.12 -
    6.13 -lemma (in bounded_linear) LIM_zero:
    6.14 -  "g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0"
    6.15 -  by (rule tendsto_zero)
    6.16 -
    6.17 -text {* Bounded Bilinear Operators *}
    6.18 -
    6.19 -lemma (in bounded_bilinear) LIM:
    6.20 -  "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"
    6.21 -by (rule tendsto)
    6.22 -
    6.23 -lemma (in bounded_bilinear) LIM_prod_zero:
    6.24 -  fixes a :: "'d::metric_space"
    6.25 -  assumes f: "f -- a --> 0"
    6.26 -  assumes g: "g -- a --> 0"
    6.27 -  shows "(\<lambda>x. f x ** g x) -- a --> 0"
    6.28 -  using f g by (rule tendsto_zero)
    6.29 -
    6.30 -lemma (in bounded_bilinear) LIM_left_zero:
    6.31 -  "f -- a --> 0 \<Longrightarrow> (\<lambda>x. f x ** c) -- a --> 0"
    6.32 -  by (rule tendsto_left_zero)
    6.33 -
    6.34 -lemma (in bounded_bilinear) LIM_right_zero:
    6.35 -  "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
    6.36 -  by (rule tendsto_right_zero)
    6.37 -
    6.38 -lemmas LIM_mult_zero =
    6.39 -  bounded_bilinear.LIM_prod_zero [OF bounded_bilinear_mult]
    6.40 -
    6.41 -lemmas LIM_mult_left_zero =
    6.42 -  bounded_bilinear.LIM_left_zero [OF bounded_bilinear_mult]
    6.43 -
    6.44 -lemmas LIM_mult_right_zero =
    6.45 -  bounded_bilinear.LIM_right_zero [OF bounded_bilinear_mult]
    6.46 -
    6.47 -lemma LIM_inverse_fun:
    6.48 -  assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)"
    6.49 -  shows "inverse -- a --> inverse a"
    6.50 -  by (rule tendsto_inverse [OF tendsto_ident_at a])
    6.51 -
    6.52  
    6.53  subsection {* Continuity *}
    6.54  
    6.55 @@ -495,29 +450,4 @@
    6.56     (X -- a --> (L::'b::topological_space))"
    6.57    using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
    6.58  
    6.59 -subsection {* Legacy theorem names *}
    6.60 -
    6.61 -lemmas LIM_ident [simp] = tendsto_ident_at
    6.62 -lemmas LIM_const [simp] = tendsto_const [where F="at x", standard]
    6.63 -lemmas LIM_add = tendsto_add [where F="at x", standard]
    6.64 -lemmas LIM_add_zero = tendsto_add_zero [where F="at x", standard]
    6.65 -lemmas LIM_minus = tendsto_minus [where F="at x", standard]
    6.66 -lemmas LIM_diff = tendsto_diff [where F="at x", standard]
    6.67 -lemmas LIM_norm = tendsto_norm [where F="at x", standard]
    6.68 -lemmas LIM_norm_zero = tendsto_norm_zero [where F="at x", standard]
    6.69 -lemmas LIM_norm_zero_cancel = tendsto_norm_zero_cancel [where F="at x", standard]
    6.70 -lemmas LIM_norm_zero_iff = tendsto_norm_zero_iff [where F="at x", standard]
    6.71 -lemmas LIM_rabs = tendsto_rabs [where F="at x", standard]
    6.72 -lemmas LIM_rabs_zero = tendsto_rabs_zero [where F="at x", standard]
    6.73 -lemmas LIM_rabs_zero_cancel = tendsto_rabs_zero_cancel [where F="at x", standard]
    6.74 -lemmas LIM_rabs_zero_iff = tendsto_rabs_zero_iff [where F="at x", standard]
    6.75 -lemmas LIM_compose = tendsto_compose [where F="at x", standard]
    6.76 -lemmas LIM_mult = tendsto_mult [where F="at x", standard]
    6.77 -lemmas LIM_scaleR = tendsto_scaleR [where F="at x", standard]
    6.78 -lemmas LIM_of_real = tendsto_of_real [where F="at x", standard]
    6.79 -lemmas LIM_power = tendsto_power [where F="at x", standard]
    6.80 -lemmas LIM_inverse = tendsto_inverse [where F="at x", standard]
    6.81 -lemmas LIM_sgn = tendsto_sgn [where F="at x", standard]
    6.82 -lemmas isCont_LIM_compose = isCont_tendsto_compose [where F="at x", standard]
    6.83 -
    6.84  end
     7.1 --- a/src/HOL/Limits.thy	Sat Aug 27 17:26:14 2011 +0200
     7.2 +++ b/src/HOL/Limits.thy	Sun Aug 28 09:20:12 2011 -0700
     7.3 @@ -791,6 +791,15 @@
     7.4  lemmas tendsto_mult [tendsto_intros] =
     7.5    bounded_bilinear.tendsto [OF bounded_bilinear_mult]
     7.6  
     7.7 +lemmas tendsto_mult_zero =
     7.8 +  bounded_bilinear.tendsto_zero [OF bounded_bilinear_mult]
     7.9 +
    7.10 +lemmas tendsto_mult_left_zero =
    7.11 +  bounded_bilinear.tendsto_left_zero [OF bounded_bilinear_mult]
    7.12 +
    7.13 +lemmas tendsto_mult_right_zero =
    7.14 +  bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult]
    7.15 +
    7.16  lemma tendsto_power [tendsto_intros]:
    7.17    fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
    7.18    shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) ---> a ^ n) F"
     8.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sat Aug 27 17:26:14 2011 +0200
     8.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Aug 28 09:20:12 2011 -0700
     8.3 @@ -47,7 +47,7 @@
     8.4    shows "FDERIV f x :> f' = (f has_derivative f') (at x)"
     8.5    unfolding fderiv_def has_derivative_def netlimit_at_vector
     8.6    by (simp add: diff_diff_eq Lim_at_zero [where a=x]
     8.7 -    LIM_norm_zero_iff [where 'b='b, symmetric])
     8.8 +    tendsto_norm_zero_iff [where 'b='b, symmetric])
     8.9  
    8.10  lemma DERIV_conv_has_derivative:
    8.11    "(DERIV f x :> f') = (f has_derivative op * f') (at x)"
     9.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Aug 27 17:26:14 2011 +0200
     9.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Aug 28 09:20:12 2011 -0700
     9.3 @@ -1332,10 +1332,10 @@
     9.4  unfolding netlimit_def
     9.5  apply (rule some_equality)
     9.6  apply (rule Lim_at_within)
     9.7 -apply (rule LIM_ident)
     9.8 +apply (rule tendsto_ident_at)
     9.9  apply (erule tendsto_unique [OF assms])
    9.10  apply (rule Lim_at_within)
    9.11 -apply (rule LIM_ident)
    9.12 +apply (rule tendsto_ident_at)
    9.13  done
    9.14  
    9.15  lemma netlimit_at:
    9.16 @@ -3569,11 +3569,11 @@
    9.17  
    9.18  lemma continuous_within_id:
    9.19   "continuous (at a within s) (\<lambda>x. x)"
    9.20 -  unfolding continuous_within by (rule Lim_at_within [OF LIM_ident])
    9.21 +  unfolding continuous_within by (rule Lim_at_within [OF tendsto_ident_at])
    9.22  
    9.23  lemma continuous_at_id:
    9.24   "continuous (at a) (\<lambda>x. x)"
    9.25 -  unfolding continuous_at by (rule LIM_ident)
    9.26 +  unfolding continuous_at by (rule tendsto_ident_at)
    9.27  
    9.28  lemma continuous_on_id:
    9.29   "continuous_on s (\<lambda>x. x)"
    9.30 @@ -4260,7 +4260,7 @@
    9.31  proof (rule continuous_attains_sup [OF assms])
    9.32    { fix x assume "x\<in>s"
    9.33      have "(dist a ---> dist a x) (at x within s)"
    9.34 -      by (intro tendsto_dist tendsto_const Lim_at_within LIM_ident)
    9.35 +      by (intro tendsto_dist tendsto_const Lim_at_within tendsto_ident_at)
    9.36    }
    9.37    thus "continuous_on s (dist a)"
    9.38      unfolding continuous_on ..
    10.1 --- a/src/HOL/NSA/HSEQ.thy	Sat Aug 27 17:26:14 2011 +0200
    10.2 +++ b/src/HOL/NSA/HSEQ.thy	Sun Aug 28 09:20:12 2011 -0700
    10.3 @@ -207,10 +207,10 @@
    10.4  text{*We prove the NS version from the standard one, since the NS proof
    10.5     seems more complicated than the standard one above!*}
    10.6  lemma NSLIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) ----NS> 0) = (X ----NS> 0)"
    10.7 -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_norm_zero)
    10.8 +by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_norm_zero_iff)
    10.9  
   10.10  lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----NS> 0) = (f ----NS> (0::real))"
   10.11 -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_rabs_zero)
   10.12 +by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_rabs_zero_iff)
   10.13  
   10.14  text{*Generalization to other limits*}
   10.15  lemma NSLIMSEQ_imp_rabs: "f ----NS> (l::real) ==> (%n. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>"
    11.1 --- a/src/HOL/Probability/Caratheodory.thy	Sat Aug 27 17:26:14 2011 +0200
    11.2 +++ b/src/HOL/Probability/Caratheodory.thy	Sun Aug 28 09:20:12 2011 -0700
    11.3 @@ -128,7 +128,7 @@
    11.4          by (induct n)  (auto simp add: binaryset_def f)
    11.5      qed
    11.6    moreover
    11.7 -  have "... ----> f A + f B" by (rule LIMSEQ_const)
    11.8 +  have "... ----> f A + f B" by (rule tendsto_const)
    11.9    ultimately
   11.10    have "(\<lambda>n. \<Sum>i< Suc (Suc n). f (binaryset A B i)) ----> f A + f B"
   11.11      by metis
   11.12 @@ -985,7 +985,7 @@
   11.13    ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) ----> 0"
   11.14      by (simp add: zero_ereal_def)
   11.15    then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
   11.16 -    by (rule LIMSEQ_diff_approach_zero2[OF LIMSEQ_const])
   11.17 +    by (rule LIMSEQ_diff_approach_zero2[OF tendsto_const])
   11.18    then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
   11.19      using A by (subst (1 2) f') auto
   11.20  qed
    12.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Sat Aug 27 17:26:14 2011 +0200
    12.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Sun Aug 28 09:20:12 2011 -0700
    12.3 @@ -2191,9 +2191,9 @@
    12.4    have 3: "\<And>x n. 0 \<le> f n x - f 0 x" using `mono f`
    12.5        unfolding mono_def le_fun_def by (auto simp: field_simps)
    12.6    have 4: "\<And>x. (\<lambda>i. f i x - f 0 x) ----> u x - f 0 x"
    12.7 -    using lim by (auto intro!: LIMSEQ_diff)
    12.8 +    using lim by (auto intro!: tendsto_diff)
    12.9    have 5: "(\<lambda>i. (\<integral>x. f i x - f 0 x \<partial>M)) ----> x - integral\<^isup>L M (f 0)"
   12.10 -    using f ilim by (auto intro!: LIMSEQ_diff simp: integral_diff)
   12.11 +    using f ilim by (auto intro!: tendsto_diff simp: integral_diff)
   12.12    note diff = integral_monotone_convergence_pos[OF 1 2 3 4 5]
   12.13    have "integrable M (\<lambda>x. (u x - f 0 x) + f 0 x)"
   12.14      using diff(1) f by (rule integral_add(1))
   12.15 @@ -2329,7 +2329,7 @@
   12.16    and "(\<lambda>i. integral\<^isup>L M (u i)) ----> integral\<^isup>L M u'" (is ?lim)
   12.17  proof -
   12.18    { fix x j assume x: "x \<in> space M"
   12.19 -    from u'[OF x] have "(\<lambda>i. \<bar>u i x\<bar>) ----> \<bar>u' x\<bar>" by (rule LIMSEQ_imp_rabs)
   12.20 +    from u'[OF x] have "(\<lambda>i. \<bar>u i x\<bar>) ----> \<bar>u' x\<bar>" by (rule tendsto_rabs)
   12.21      from LIMSEQ_le_const2[OF this]
   12.22      have "\<bar>u' x\<bar> \<le> w x" using bound[OF x] by auto }
   12.23    note u'_bound = this
   12.24 @@ -2400,7 +2400,7 @@
   12.25          unfolding ereal_max_0
   12.26        proof (rule lim_imp_Liminf[symmetric], unfold lim_ereal)
   12.27          have "(\<lambda>i. ?diff i x) ----> 2 * w x - \<bar>u' x - u' x\<bar>"
   12.28 -          using u'[OF x] by (safe intro!: LIMSEQ_diff LIMSEQ_const LIMSEQ_imp_rabs)
   12.29 +          using u'[OF x] by (safe intro!: tendsto_intros)
   12.30          then show "(\<lambda>i. max 0 (?diff i x)) ----> max 0 (2 * w x)"
   12.31            by (auto intro!: tendsto_real_max simp add: lim_ereal)
   12.32        qed (rule trivial_limit_sequentially)
   12.33 @@ -2492,7 +2492,7 @@
   12.34      show "mono ?w'"
   12.35        by (auto simp: mono_def le_fun_def intro!: setsum_mono2)
   12.36      { fix x show "(\<lambda>n. ?w' n x) ----> ?w x"
   12.37 -        using w by (cases "x \<in> space M") (simp_all add: LIMSEQ_const sums_def) }
   12.38 +        using w by (cases "x \<in> space M") (simp_all add: tendsto_const sums_def) }
   12.39      have *: "\<And>n. integral\<^isup>L M (?w' n) = (\<Sum>i = 0..< n. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
   12.40        using borel by (simp add: integral_setsum integrable_abs cong: integral_cong)
   12.41      from abs_sum
    13.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Sat Aug 27 17:26:14 2011 +0200
    13.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Sun Aug 28 09:20:12 2011 -0700
    13.3 @@ -209,7 +209,7 @@
    13.4      from finite_continuity_from_below[OF _ A] `range A \<subseteq> sets M`
    13.5        M'.finite_continuity_from_below[OF _ A]
    13.6      have convergent: "(\<lambda>i. ?d (A i)) ----> ?d (\<Union>i. A i)"
    13.7 -      by (auto intro!: LIMSEQ_diff)
    13.8 +      by (auto intro!: tendsto_diff)
    13.9      obtain n :: nat where "- ?d (\<Union>i. A i) / e < real n" using reals_Archimedean2 by auto
   13.10      moreover from order_trans[OF decseq_le[OF decseq convergent] dA_less]
   13.11      have "real n \<le> - ?d (\<Union>i. A i) / e" using `0<e` by (simp add: field_simps)
   13.12 @@ -295,7 +295,7 @@
   13.13      from
   13.14        finite_continuity_from_above[OF `range A \<subseteq> sets M` A]
   13.15        M'.finite_continuity_from_above[OF `range A \<subseteq> sets M` A]
   13.16 -    have "(\<lambda>i. ?d (A i)) ----> ?d (\<Inter>i. A i)" by (intro LIMSEQ_diff)
   13.17 +    have "(\<lambda>i. ?d (A i)) ----> ?d (\<Inter>i. A i)" by (intro tendsto_diff)
   13.18      thus "?d (space M) \<le> ?d (\<Inter>i. A i)" using mono_dA[THEN monoD, of 0 _]
   13.19        by (rule_tac LIMSEQ_le_const) (auto intro!: exI)
   13.20    next
    14.1 --- a/src/HOL/SEQ.thy	Sat Aug 27 17:26:14 2011 +0200
    14.2 +++ b/src/HOL/SEQ.thy	Sun Aug 28 09:20:12 2011 -0700
    14.3 @@ -772,7 +772,7 @@
    14.4    have X: "!!n. X n = X 0"
    14.5      by (blast intro: const [of 0]) 
    14.6    have "X = (\<lambda>n. X 0)"
    14.7 -    by (blast intro: ext X)
    14.8 +    by (blast intro: X)
    14.9    hence "L = X 0" using tendsto_const [of "X 0" sequentially]
   14.10      by (auto intro: LIMSEQ_unique lim)
   14.11    thus ?thesis
   14.12 @@ -1144,25 +1144,4 @@
   14.13  apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs)
   14.14  done
   14.15  
   14.16 -subsection {* Legacy theorem names *}
   14.17 -
   14.18 -lemmas LIMSEQ_Zfun_iff = tendsto_Zfun_iff [where F=sequentially]
   14.19 -lemmas LIMSEQ_const = tendsto_const [where F=sequentially]
   14.20 -lemmas LIMSEQ_norm = tendsto_norm [where F=sequentially]
   14.21 -lemmas LIMSEQ_add = tendsto_add [where F=sequentially]
   14.22 -lemmas LIMSEQ_minus = tendsto_minus [where F=sequentially]
   14.23 -lemmas LIMSEQ_minus_cancel = tendsto_minus_cancel [where F=sequentially]
   14.24 -lemmas LIMSEQ_diff = tendsto_diff [where F=sequentially]
   14.25 -lemmas (in bounded_linear) LIMSEQ = tendsto [where F=sequentially]
   14.26 -lemmas (in bounded_bilinear) LIMSEQ = tendsto [where F=sequentially]
   14.27 -lemmas LIMSEQ_mult = tendsto_mult [where F=sequentially]
   14.28 -lemmas LIMSEQ_inverse = tendsto_inverse [where F=sequentially]
   14.29 -lemmas LIMSEQ_divide = tendsto_divide [where F=sequentially]
   14.30 -lemmas LIMSEQ_pow = tendsto_power [where F=sequentially]
   14.31 -lemmas LIMSEQ_setsum = tendsto_setsum [where F=sequentially]
   14.32 -lemmas LIMSEQ_setprod = tendsto_setprod [where F=sequentially]
   14.33 -lemmas LIMSEQ_norm_zero = tendsto_norm_zero_iff [where F=sequentially]
   14.34 -lemmas LIMSEQ_rabs_zero = tendsto_rabs_zero_iff [where F=sequentially]
   14.35 -lemmas LIMSEQ_imp_rabs = tendsto_rabs [where F=sequentially]
   14.36 -
   14.37  end
    15.1 --- a/src/HOL/Series.thy	Sat Aug 27 17:26:14 2011 +0200
    15.2 +++ b/src/HOL/Series.thy	Sun Aug 28 09:20:12 2011 -0700
    15.3 @@ -183,12 +183,12 @@
    15.4      unfolding sums_def
    15.5      apply (rule LIMSEQ_offset[of _ n])
    15.6      unfolding setsum_const
    15.7 -    apply (rule LIMSEQ_const)
    15.8 +    apply (rule tendsto_const)
    15.9      done
   15.10  qed
   15.11  
   15.12  lemma sums_zero[simp, intro]: "(\<lambda>n. 0) sums 0"
   15.13 -unfolding sums_def by (simp add: LIMSEQ_const)
   15.14 +  unfolding sums_def by (simp add: tendsto_const)
   15.15  
   15.16  lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)"
   15.17  by (rule sums_zero [THEN sums_summable])
   15.18 @@ -198,7 +198,7 @@
   15.19  
   15.20  lemma (in bounded_linear) sums:
   15.21    "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)"
   15.22 -unfolding sums_def by (drule LIMSEQ, simp only: setsum)
   15.23 +  unfolding sums_def by (drule tendsto, simp only: setsum)
   15.24  
   15.25  lemma (in bounded_linear) summable:
   15.26    "summable (\<lambda>n. X n) \<Longrightarrow> summable (\<lambda>n. f (X n))"
   15.27 @@ -260,7 +260,7 @@
   15.28  lemma sums_add:
   15.29    fixes a b :: "'a::real_normed_field"
   15.30    shows "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) sums (a + b)"
   15.31 -unfolding sums_def by (simp add: setsum_addf LIMSEQ_add)
   15.32 +  unfolding sums_def by (simp add: setsum_addf tendsto_add)
   15.33  
   15.34  lemma summable_add:
   15.35    fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field"
   15.36 @@ -275,7 +275,7 @@
   15.37  lemma sums_diff:
   15.38    fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field"
   15.39    shows "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) sums (a - b)"
   15.40 -unfolding sums_def by (simp add: setsum_subtractf LIMSEQ_diff)
   15.41 +  unfolding sums_def by (simp add: setsum_subtractf tendsto_diff)
   15.42  
   15.43  lemma summable_diff:
   15.44    fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field"
   15.45 @@ -290,7 +290,7 @@
   15.46  lemma sums_minus:
   15.47    fixes X :: "nat \<Rightarrow> 'a::real_normed_field"
   15.48    shows "X sums a ==> (\<lambda>n. - X n) sums (- a)"
   15.49 -unfolding sums_def by (simp add: setsum_negf LIMSEQ_minus)
   15.50 +  unfolding sums_def by (simp add: setsum_negf tendsto_minus)
   15.51  
   15.52  lemma summable_minus:
   15.53    fixes X :: "nat \<Rightarrow> 'a::real_normed_field"
   15.54 @@ -344,7 +344,7 @@
   15.55    shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 \<le> f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} \<le> suminf f"
   15.56  apply (drule summable_sums)
   15.57  apply (simp add: sums_def)
   15.58 -apply (cut_tac k = "setsum f {0..<n}" in LIMSEQ_const)
   15.59 +apply (cut_tac k = "setsum f {0..<n}" in tendsto_const)
   15.60  apply (erule LIMSEQ_le, blast)
   15.61  apply (rule_tac x="n" in exI, clarify)
   15.62  apply (rule setsum_mono2)
   15.63 @@ -403,7 +403,7 @@
   15.64    from less_1 have lim_0: "(\<lambda>n. x ^ n) ----> 0"
   15.65      by (rule LIMSEQ_power_zero)
   15.66    hence "(\<lambda>n. x ^ n / (x - 1) - 1 / (x - 1)) ----> 0 / (x - 1) - 1 / (x - 1)"
   15.67 -    using neq_0 by (intro LIMSEQ_divide LIMSEQ_diff LIMSEQ_const)
   15.68 +    using neq_0 by (intro tendsto_intros)
   15.69    hence "(\<lambda>n. (x ^ n - 1) / (x - 1)) ----> 1 / (1 - x)"
   15.70      by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib)
   15.71    thus "(\<lambda>n. x ^ n) sums (1 / (1 - x))"
   15.72 @@ -583,7 +583,7 @@
   15.73  lemma summable_norm:
   15.74    fixes f :: "nat \<Rightarrow> 'a::banach"
   15.75    shows "summable (\<lambda>n. norm (f n)) \<Longrightarrow> norm (suminf f) \<le> (\<Sum>n. norm (f n))"
   15.76 -by (auto intro: LIMSEQ_le LIMSEQ_norm summable_norm_cancel
   15.77 +  by (auto intro: LIMSEQ_le tendsto_norm summable_norm_cancel
   15.78                  summable_sumr_LIMSEQ_suminf norm_setsum)
   15.79  
   15.80  lemma summable_rabs:
   15.81 @@ -692,7 +692,7 @@
   15.82  
   15.83    have "(\<lambda>n. (\<Sum>k=0..<n. a k) * (\<Sum>k=0..<n. b k))
   15.84             ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
   15.85 -    by (intro LIMSEQ_mult summable_sumr_LIMSEQ_suminf
   15.86 +    by (intro tendsto_mult summable_sumr_LIMSEQ_suminf
   15.87          summable_norm_cancel [OF a] summable_norm_cancel [OF b])
   15.88    hence 1: "(\<lambda>n. setsum ?g (?S1 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
   15.89      by (simp only: setsum_product setsum_Sigma [rule_format]
   15.90 @@ -700,7 +700,7 @@
   15.91  
   15.92    have "(\<lambda>n. (\<Sum>k=0..<n. norm (a k)) * (\<Sum>k=0..<n. norm (b k)))
   15.93         ----> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
   15.94 -    using a b by (intro LIMSEQ_mult summable_sumr_LIMSEQ_suminf)
   15.95 +    using a b by (intro tendsto_mult summable_sumr_LIMSEQ_suminf)
   15.96    hence "(\<lambda>n. setsum ?f (?S1 n)) ----> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
   15.97      by (simp only: setsum_product setsum_Sigma [rule_format]
   15.98                     finite_atLeastLessThan)
    16.1 --- a/src/HOL/Transcendental.thy	Sat Aug 27 17:26:14 2011 +0200
    16.2 +++ b/src/HOL/Transcendental.thy	Sun Aug 28 09:20:12 2011 -0700
    16.3 @@ -294,7 +294,7 @@
    16.4      hence ord: "\<And>n m. m \<le> n \<Longrightarrow> ?a n \<le> ?a m" and ge0: "\<And> n. 0 \<le> ?a n" by auto
    16.5      { fix n have "?a (Suc n) \<le> ?a n" using ord[where n="Suc n" and m=n] by auto }
    16.6      note monotone = this
    16.7 -    note leibniz = summable_Leibniz'[OF _ ge0, of "\<lambda>x. x", OF LIMSEQ_minus[OF `a ----> 0`, unfolded minus_zero] monotone]
    16.8 +    note leibniz = summable_Leibniz'[OF _ ge0, of "\<lambda>x. x", OF tendsto_minus[OF `a ----> 0`, unfolded minus_zero] monotone]
    16.9      have "summable (\<lambda> n. (-1)^n * ?a n)" using leibniz(1) by auto
   16.10      then obtain l where "(\<lambda> n. (-1)^n * ?a n) sums l" unfolding summable_def by auto
   16.11      from this[THEN sums_minus]
   16.12 @@ -308,7 +308,7 @@
   16.13  
   16.14      have ?pos using `0 \<le> ?a 0` by auto
   16.15      moreover have ?neg using leibniz(2,4) unfolding mult_minus_right setsum_negf move_minus neg_le_iff_le by auto
   16.16 -    moreover have ?f and ?g using leibniz(3,5)[unfolded mult_minus_right setsum_negf move_minus, THEN LIMSEQ_minus_cancel] by auto
   16.17 +    moreover have ?f and ?g using leibniz(3,5)[unfolded mult_minus_right setsum_negf move_minus, THEN tendsto_minus_cancel] by auto
   16.18      ultimately show ?thesis by auto
   16.19    qed
   16.20    from this[THEN conjunct1] this[THEN conjunct2, THEN conjunct1] this[THEN conjunct2, THEN conjunct2, THEN conjunct1] this[THEN conjunct2, THEN conjunct2, THEN conjunct2, THEN conjunct1]
   16.21 @@ -2582,21 +2582,21 @@
   16.22  
   16.23  lemma zeroseq_arctan_series: fixes x :: real
   16.24    assumes "\<bar>x\<bar> \<le> 1" shows "(\<lambda> n. 1 / real (n*2+1) * x^(n*2+1)) ----> 0" (is "?a ----> 0")
   16.25 -proof (cases "x = 0") case True thus ?thesis unfolding One_nat_def by (auto simp add: LIMSEQ_const)
   16.26 +proof (cases "x = 0") case True thus ?thesis unfolding One_nat_def by (auto simp add: tendsto_const)
   16.27  next
   16.28    case False
   16.29    have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
   16.30    show "?a ----> 0"
   16.31    proof (cases "\<bar>x\<bar> < 1")
   16.32      case True hence "norm x < 1" by auto
   16.33 -    from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]]
   16.34 +    from tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]]
   16.35      have "(\<lambda>n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0"
   16.36        unfolding inverse_eq_divide Suc_eq_plus1 by simp
   16.37      then show ?thesis using pos2 by (rule LIMSEQ_linear)
   16.38    next
   16.39      case False hence "x = -1 \<or> x = 1" using `\<bar>x\<bar> \<le> 1` by auto
   16.40      hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x" unfolding One_nat_def by auto
   16.41 -    from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] LIMSEQ_const[of x]]
   16.42 +    from tendsto_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] tendsto_const[of x]]
   16.43      show ?thesis unfolding n_eq Suc_eq_plus1 by auto
   16.44    qed
   16.45  qed
   16.46 @@ -2775,8 +2775,8 @@
   16.47        hence "?diff 1 n \<le> ?a 1 n" by auto
   16.48      }
   16.49      have "?a 1 ----> 0"
   16.50 -      unfolding LIMSEQ_rabs_zero power_one divide_inverse One_nat_def
   16.51 -      by (auto intro!: LIMSEQ_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
   16.52 +      unfolding tendsto_rabs_zero_iff power_one divide_inverse One_nat_def
   16.53 +      by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
   16.54      have "?diff 1 ----> 0"
   16.55      proof (rule LIMSEQ_I)
   16.56        fix r :: real assume "0 < r"
   16.57 @@ -2785,7 +2785,7 @@
   16.58          have "norm (?diff 1 n - 0) < r" by auto }
   16.59        thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
   16.60      qed
   16.61 -    from this[unfolded LIMSEQ_rabs_zero diff_minus add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN LIMSEQ_minus]
   16.62 +    from this[unfolded tendsto_rabs_zero_iff diff_minus add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN tendsto_minus]
   16.63      have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
   16.64      hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
   16.65