# HG changeset patch
# User huffman
# Date 1313017008 25200
# Node ID abccf1b7ea4ba40b680efbda9ab8e83ded4d0b31
# Parent  0c9feac80852253733319b28f0031b1ac25b979f
remove redundant lemma

diff -r 0c9feac80852 -r abccf1b7ea4b src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 10 14:25:56 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 10 15:56:48 2011 -0700
@@ -1031,9 +1031,6 @@
           (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (S n) l < e)"
   by (auto simp add: tendsto_iff eventually_sequentially)
 
-lemma Lim_sequentially_iff_LIMSEQ: "(S ---> l) sequentially \<longleftrightarrow> S ----> l"
-  unfolding Lim_sequentially LIMSEQ_def ..
-
 lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
   by (rule topological_tendstoI, auto elim: eventually_rev_mono)