changeset 44522 | 2f7e9d890efe |
parent 44521 | 083eedb37a37 |
child 44571 | bd91b77c4cd6 |
--- 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