diff -r 5e5e6ad3922c -r e6f291cb5810 NEWS
--- a/NEWS	Sat Aug 27 17:26:14 2011 +0200
+++ b/NEWS	Sun Aug 28 09:20:12 2011 -0700
@@ -246,8 +246,8 @@
   mult_right.setsum ~> setsum_right_distrib
   mult_left.diff ~> left_diff_distrib
 
-* Complex_Main: Several redundant theorems about real numbers have
-been removed or generalized and renamed. INCOMPATIBILITY.
+* Complex_Main: Several redundant theorems have been removed or
+replaced by more general versions. INCOMPATIBILITY.
 
   real_0_le_divide_iff ~> zero_le_divide_iff
   realpow_two_disj ~> power2_eq_iff
@@ -255,6 +255,53 @@
   realpow_two_diff ~> square_diff_square_factored
   exp_ln_eq ~> ln_unique
   lemma_DERIV_subst ~> DERIV_cong
+  LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff
+  LIMSEQ_const ~> tendsto_const
+  LIMSEQ_norm ~> tendsto_norm
+  LIMSEQ_add ~> tendsto_add
+  LIMSEQ_minus ~> tendsto_minus
+  LIMSEQ_minus_cancel ~> tendsto_minus_cancel
+  LIMSEQ_diff ~> tendsto_diff
+  bounded_linear.LIMSEQ ~> bounded_linear.tendsto
+  bounded_bilinear.LIMSEQ ~> bounded_bilinear.tendsto
+  LIMSEQ_mult ~> tendsto_mult
+  LIMSEQ_inverse ~> tendsto_inverse
+  LIMSEQ_divide ~> tendsto_divide
+  LIMSEQ_pow ~> tendsto_power
+  LIMSEQ_setsum ~> tendsto_setsum
+  LIMSEQ_setprod ~> tendsto_setprod
+  LIMSEQ_norm_zero ~> tendsto_norm_zero_iff
+  LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff
+  LIMSEQ_imp_rabs ~> tendsto_rabs
+  LIM_ident ~> tendsto_ident_at
+  LIM_const ~> tendsto_const
+  LIM_add ~> tendsto_add
+  LIM_add_zero ~> tendsto_add_zero
+  LIM_minus ~> tendsto_minus
+  LIM_diff ~> tendsto_diff
+  LIM_norm ~> tendsto_norm
+  LIM_norm_zero ~> tendsto_norm_zero
+  LIM_norm_zero_cancel ~> tendsto_norm_zero_cancel
+  LIM_norm_zero_iff ~> tendsto_norm_zero_iff
+  LIM_rabs ~> tendsto_rabs
+  LIM_rabs_zero ~> tendsto_rabs_zero
+  LIM_rabs_zero_cancel ~> tendsto_rabs_zero_cancel
+  LIM_rabs_zero_iff ~> tendsto_rabs_zero_iff
+  LIM_compose ~> tendsto_compose
+  LIM_mult ~> tendsto_mult
+  LIM_scaleR ~> tendsto_scaleR
+  LIM_of_real ~> tendsto_of_real
+  LIM_power ~> tendsto_power
+  LIM_inverse ~> tendsto_inverse
+  LIM_sgn ~> tendsto_sgn
+  isCont_LIM_compose ~> isCont_tendsto_compose
+  bounded_linear.LIM ~> bounded_linear.tendsto
+  bounded_linear.LIM_zero ~> bounded_linear.tendsto_zero
+  bounded_bilinear.LIM ~> bounded_bilinear.tendsto
+  bounded_bilinear.LIM_prod_zero ~> bounded_bilinear.tendsto_zero
+  bounded_bilinear.LIM_left_zero ~> bounded_bilinear.tendsto_left_zero
+  bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero
+  LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at]
 
 
 *** Document preparation ***