# HG changeset patch
# User huffman
# Date 1272933586 25200
# Node ID 88f0125c3bd27200ab802f1a17c6e97e2ea289f5
# Parent  7c8eb32724ced5ef1f917a884d88af78184a0b9d
remove unneeded premise

diff -r 7c8eb32724ce -r 88f0125c3bd2 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon May 03 17:13:37 2010 -0700
+++ b/src/HOL/Limits.thy	Mon May 03 17:39:46 2010 -0700
@@ -585,7 +585,7 @@
 unfolding tendsto_def eventually_at_topological by auto
 
 lemma tendsto_ident_at_within [tendsto_intros]:
-  "a \<in> S \<Longrightarrow> ((\<lambda>x. x) ---> a) (at a within S)"
+  "((\<lambda>x. x) ---> a) (at a within S)"
 unfolding tendsto_def eventually_within eventually_at_topological by auto
 
 lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) net"