src/HOL/Lim.thy
changeset 31488 5691ccb8d6b5
parent 31487 93938cafc0e6
child 32436 10cd49e0c067
     1.1 --- a/src/HOL/Lim.thy	Fri Jun 05 15:59:20 2009 -0700
     1.2 +++ b/src/HOL/Lim.thy	Sat Jun 06 09:11:12 2009 -0700
     1.3 @@ -30,7 +30,7 @@
     1.4  subsection {* Limits of Functions *}
     1.5  
     1.6  lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> (f ---> L) (at a)"
     1.7 -unfolding LIM_def tendsto_def eventually_at ..
     1.8 +unfolding LIM_def tendsto_iff eventually_at ..
     1.9  
    1.10  lemma metric_LIM_I:
    1.11    "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)