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