src/HOL/Lim.thy
changeset 32650 34bfa2492298
parent 32642 026e7c6a6d08
child 36661 0a5b7b818d65
     1.1 --- a/src/HOL/Lim.thy	Wed Sep 23 11:06:32 2009 +0100
     1.2 +++ b/src/HOL/Lim.thy	Wed Sep 23 13:17:17 2009 +0200
     1.3 @@ -84,6 +84,8 @@
     1.4  lemma LIM_const [simp]: "(%x. k) -- x --> k"
     1.5  by (simp add: LIM_def)
     1.6  
     1.7 +lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp
     1.8 +
     1.9  lemma LIM_add:
    1.10    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.11    assumes f: "f -- a --> L" and g: "g -- a --> M"