src/HOL/Lim.thy

--- a/src/HOL/Lim.thy	Wed Sep 23 11:06:32 2009 +0100
+++ b/src/HOL/Lim.thy	Wed Sep 23 13:17:17 2009 +0200
@@ -84,6 +84,8 @@
 lemma LIM_const [simp]: "(%x. k) -- x --> k"
 by (simp add: LIM_def)
 
+lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp
+
 lemma LIM_add:
   fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   assumes f: "f -- a --> L" and g: "g -- a --> M"