--- 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