# HG changeset patch # User huffman # Date 1272992194 25200 # Node ID f794e92784aaedeb7c8fe012a1812dd00c5c9bd2 # Parent e37b4338c71fa2f0d615ba02380fbe0a163ad37f adapt to removed premise on tendsto lemma (cf. 88f0125c3bd2) diff -r e37b4338c71f -r f794e92784aa src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue May 04 09:41:29 2010 -0700 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue May 04 09:56:34 2010 -0700 @@ -5336,7 +5336,7 @@ unfolding dist_norm apply (auto simp add: pos_divide_less_eq mult_strict_left_mono) unfolding continuous_on - by (intro ballI tendsto_intros, simp, assumption)+ + by (intro ballI tendsto_intros, simp)+ next have *:"\e / d\ > 0" "\d / e\ >0" using assms using divide_pos_pos by auto show ?cth unfolding homeomorphic_minimal @@ -5346,7 +5346,7 @@ unfolding dist_norm apply (auto simp add: pos_divide_le_eq) unfolding continuous_on - by (intro ballI tendsto_intros, simp, assumption)+ + by (intro ballI tendsto_intros, simp)+ qed text{* "Isometry" (up to constant bounds) of injective linear map etc. *}