diff -r 083eedb37a37 -r 2f7e9d890efe src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 25 11:57:42 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 25 12:43:55 2011 -0700
@@ -2001,8 +2001,4 @@
     apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe)
     apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed
 
-text {* Legacy theorem names *}
-
-lemmas Lim_component_cart = tendsto_vec_nth
-
 end