| changeset 31487 | 93938cafc0e6 |
| parent 31392 | 69570155ddf8 |
| child 31488 | 5691ccb8d6b5 |
--- a/src/HOL/Lim.thy Fri Jun 05 21:55:08 2009 +0200 +++ b/src/HOL/Lim.thy Fri Jun 05 15:59:20 2009 -0700 @@ -29,7 +29,7 @@ subsection {* Limits of Functions *} -lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> tendsto f L (at a)" +lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> (f ---> L) (at a)" unfolding LIM_def tendsto_def eventually_at .. lemma metric_LIM_I: