Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove unneeded premise
authorhuffman
Mon, 03 May 2010 17:39:46 -0700
changeset 36655 88f0125c3bd2
parent 36654 7c8eb32724ce
child 36656 fec55067ae9b
remove unneeded premise
src/HOL/Limits.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle