src/HOL/Lim.thy
changeset 44251 d101ed3177b6
parent 44233 aa74ce315bae
child 44253 c073a0bd8458
     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"