src/HOL/Lim.thy
changeset 29667 53103fc8ffa3
parent 29197 6d4cb27ed19c
child 29803 c56a5571f60a
     1.1 --- a/src/HOL/Lim.thy	Sun Jan 18 13:58:17 2009 +0100
     1.2 +++ b/src/HOL/Lim.thy	Wed Jan 28 16:29:16 2009 +0100
     1.3 @@ -52,7 +52,7 @@
     1.4  apply (drule_tac r="r" in LIM_D, safe)
     1.5  apply (rule_tac x="s" in exI, safe)
     1.6  apply (drule_tac x="x + k" in spec)
     1.7 -apply (simp add: compare_rls)
     1.8 +apply (simp add: algebra_simps)
     1.9  done
    1.10  
    1.11  lemma LIM_offset_zero: "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"