1.1 --- a/src/HOL/Lim.thy	Wed Aug 17 09:59:10 2011 -0700
     1.2 +++ b/src/HOL/Lim.thy	Wed Aug 17 11:06:39 2011 -0700
     1.3 @@ -132,12 +132,8 @@
     1.4    assumes f: "f -- a --> l"
     1.5    assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l"
     1.6    shows "g -- a --> m"
     1.7 -apply (rule tendstoI, drule tendstoD [OF f])
     1.8 -apply (simp add: eventually_at_topological, safe)
     1.9 -apply (rule_tac x="S" in exI, safe)
    1.10 -apply (drule_tac x="x" in bspec, safe)
    1.11 -apply (erule (1) order_le_less_trans [OF le])
    1.12 -done
    1.13 +  by (rule metric_tendsto_imp_tendsto [OF f],
    1.14 +    auto simp add: eventually_at_topological le)
    1.15  
    1.16  lemma LIM_imp_LIM:
    1.17    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.18 @@ -145,9 +141,8 @@
    1.19    assumes f: "f -- a --> l"
    1.20    assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
    1.21    shows "g -- a --> m"
    1.22 -apply (rule metric_LIM_imp_LIM [OF f])
    1.23 -apply (simp add: dist_norm le)
    1.24 -done
    1.25 +  by (rule metric_LIM_imp_LIM [OF f],
    1.26 +    simp add: dist_norm le)
    1.27  
    1.28  lemma LIM_norm:
    1.29    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"

     2.1 --- a/src/HOL/Limits.thy	Wed Aug 17 09:59:10 2011 -0700
     2.2 +++ b/src/HOL/Limits.thy	Wed Aug 17 11:06:39 2011 -0700
     2.3 @@ -627,6 +627,17 @@
     2.4      by (rule eventually_mono)
     2.5  qed
     2.6  
     2.7 +lemma metric_tendsto_imp_tendsto:
     2.8 +  assumes f: "(f ---> a) F"
     2.9 +  assumes le: "eventually (\<lambda>x. dist (g x) b \<le> dist (f x) a) F"
    2.10 +  shows "(g ---> b) F"
    2.11 +proof (rule tendstoI)
    2.12 +  fix e :: real assume "0 < e"
    2.13 +  with f have "eventually (\<lambda>x. dist (f x) a < e) F" by (rule tendstoD)
    2.14 +  with le show "eventually (\<lambda>x. dist (g x) b < e) F"
    2.15 +    using le_less_trans by (rule eventually_elim2)
    2.16 +qed
    2.17 +
    2.18  subsubsection {* Distance and norms *}
    2.19  
    2.20  lemma tendsto_dist [tendsto_intros]: