diff -r f794e92784aa -r 1cc4ab4b7ff7 src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Tue May 04 09:56:34 2010 -0700
+++ b/src/HOL/Library/Product_Vector.thy	Tue May 04 10:06:05 2010 -0700
@@ -312,18 +312,6 @@
        (simp add: subsetD [OF `A \<times> B \<subseteq> S`])
 qed
 
-lemma LIMSEQ_fst: "(X ----> a) \<Longrightarrow> (\<lambda>n. fst (X n)) ----> fst a"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_fst)
-
-lemma LIMSEQ_snd: "(X ----> a) \<Longrightarrow> (\<lambda>n. snd (X n)) ----> snd a"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_snd)
-
-lemma LIMSEQ_Pair:
-  assumes "X ----> a" and "Y ----> b"
-  shows "(\<lambda>n. (X n, Y n)) ----> (a, b)"
-using assms unfolding LIMSEQ_conv_tendsto
-by (rule tendsto_Pair)
-
 lemma LIM_fst: "f -- x --> a \<Longrightarrow> (\<lambda>x. fst (f x)) -- x --> fst a"
 unfolding LIM_conv_tendsto by (rule tendsto_fst)
 
@@ -374,7 +362,7 @@
     using Cauchy_snd [OF `Cauchy X`]
     by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
   have "X ----> (lim (\<lambda>n. fst (X n)), lim (\<lambda>n. snd (X n)))"
-    using LIMSEQ_Pair [OF 1 2] by simp
+    using tendsto_Pair [OF 1 2] by simp
   then show "convergent X"
     by (rule convergentI)
 qed