# 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 *:"\<bar>e / d\<bar> > 0" "\<bar>d / e\<bar> >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.           *}