1.1 --- a/src/HOL/Lim.thy	Sun Aug 28 09:22:42 2011 -0700
     1.2 +++ b/src/HOL/Lim.thy	Sun Aug 28 16:28:07 2011 -0700
     1.3 @@ -85,17 +85,17 @@
     1.4  
     1.5  lemma LIM_zero:
     1.6    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
     1.7 -  shows "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0"
     1.8 +  shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F"
     1.9  unfolding tendsto_iff dist_norm by simp
    1.10  
    1.11  lemma LIM_zero_cancel:
    1.12    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.13 -  shows "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l"
    1.14 +  shows "((\<lambda>x. f x - l) ---> 0) F \<Longrightarrow> (f ---> l) F"
    1.15  unfolding tendsto_iff dist_norm by simp
    1.16  
    1.17  lemma LIM_zero_iff:
    1.18    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.19 -  shows "(\<lambda>x. f x - l) -- a --> 0 = f -- a --> l"
    1.20 +  shows "((\<lambda>x. f x - l) ---> 0) F = (f ---> l) F"
    1.21  unfolding tendsto_iff dist_norm by simp
    1.22  
    1.23  lemma metric_LIM_imp_LIM: