remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex

--- a/NEWS	Tue Sep 06 07:41:15 2011 -0700
+++ b/NEWS	Tue Sep 06 07:45:18 2011 -0700
@@ -301,6 +301,7 @@
   LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus]
   LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const]
   LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const]
+  LIMSEQ_Complex ~> tendsto_Complex
   LIM_ident ~> tendsto_ident_at
   LIM_const ~> tendsto_const
   LIM_add ~> tendsto_add

--- a/src/HOL/Complex.thy	Tue Sep 06 07:41:15 2011 -0700
+++ b/src/HOL/Complex.thy	Tue Sep 06 07:45:18 2011 -0700
@@ -366,10 +366,6 @@
        (simp add: dist_norm real_sqrt_sum_squares_less)
 qed
 
-lemma LIMSEQ_Complex:
-  "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. Complex (X n) (Y n)) ----> Complex a b"
-  by (rule tendsto_Complex)
-
 instance complex :: banach
 proof
   fix X :: "nat \<Rightarrow> complex"
@@ -379,7 +375,7 @@
   from Cauchy_Im [OF X] have 2: "(\<lambda>n. Im (X n)) ----> lim (\<lambda>n. Im (X n))"
     by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
   have "X ----> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
-    using LIMSEQ_Complex [OF 1 2] by simp
+    using tendsto_Complex [OF 1 2] by simp
   thus "convergent X"
     by (rule convergentI)
 qed