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