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