1.1 --- a/src/HOL/Limits.thy	Tue Apr 09 14:04:41 2013 +0200
     1.2 +++ b/src/HOL/Limits.thy	Tue Apr 09 14:04:47 2013 +0200
     1.3 @@ -1532,6 +1532,11 @@
     1.4    shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
     1.5  by (drule_tac k="- a" in LIM_offset, simp)
     1.6  
     1.7 +lemma LIM_offset_zero_iff:
     1.8 +  fixes f :: "'a :: real_normed_vector \<Rightarrow> _"
     1.9 +  shows  "f -- a --> L \<longleftrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
    1.10 +  using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto
    1.11 +
    1.12  lemma LIM_zero:
    1.13    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.14    shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F"