src/HOL/Limits.thy
changeset 36655 88f0125c3bd2
parent 36654 7c8eb32724ce
child 36656 fec55067ae9b
     1.1 --- a/src/HOL/Limits.thy	Mon May 03 17:13:37 2010 -0700
     1.2 +++ b/src/HOL/Limits.thy	Mon May 03 17:39:46 2010 -0700
     1.3 @@ -585,7 +585,7 @@
     1.4  unfolding tendsto_def eventually_at_topological by auto
     1.5  
     1.6  lemma tendsto_ident_at_within [tendsto_intros]:
     1.7 -  "a \<in> S \<Longrightarrow> ((\<lambda>x. x) ---> a) (at a within S)"
     1.8 +  "((\<lambda>x. x) ---> a) (at a within S)"
     1.9  unfolding tendsto_def eventually_within eventually_at_topological by auto
    1.10  
    1.11  lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) net"