src/HOL/SEQ.thy
changeset 31487 93938cafc0e6
parent 31404 05d2eddc5d41
child 31488 5691ccb8d6b5
     1.1 --- a/src/HOL/SEQ.thy	Fri Jun 05 21:55:08 2009 +0200
     1.2 +++ b/src/HOL/SEQ.thy	Fri Jun 05 15:59:20 2009 -0700
     1.3 @@ -193,7 +193,7 @@
     1.4  
     1.5  subsection {* Limits of Sequences *}
     1.6  
     1.7 -lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> tendsto X L sequentially"
     1.8 +lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> (X ---> L) sequentially"
     1.9  unfolding LIMSEQ_def tendsto_def eventually_sequentially ..
    1.10  
    1.11  lemma LIMSEQ_iff: