diff -r d2abf6f6f619 -r da5a5589418e src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Thu Jun 11 10:37:02 2009 -0700
+++ b/src/HOL/Library/Product_Vector.thy	Thu Jun 11 11:51:12 2009 -0700
@@ -177,7 +177,7 @@
 lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y"
 unfolding dist_prod_def by simp
 
-lemma tendsto_fst:
+lemma tendsto_fst [tendsto_intros]:
   assumes "(f ---> a) net"
   shows "((\<lambda>x. fst (f x)) ---> fst a) net"
 proof (rule topological_tendstoI)
@@ -196,7 +196,7 @@
     by simp
 qed
 
-lemma tendsto_snd:
+lemma tendsto_snd [tendsto_intros]:
   assumes "(f ---> a) net"
   shows "((\<lambda>x. snd (f x)) ---> snd a) net"
 proof (rule topological_tendstoI)
@@ -215,7 +215,7 @@
     by simp
 qed
 
-lemma tendsto_Pair:
+lemma tendsto_Pair [tendsto_intros]:
   assumes "(f ---> a) net" and "(g ---> b) net"
   shows "((\<lambda>x. (f x, g x)) ---> (a, b)) net"
 proof (rule topological_tendstoI)