src/HOL/Lim.thy
changeset 45031 9583f2b56f85
parent 44571 bd91b77c4cd6
child 50331 4b6dc5077e98
     1.1 --- a/src/HOL/Lim.thy	Tue Sep 20 15:23:17 2011 +0200
     1.2 +++ b/src/HOL/Lim.thy	Tue Sep 20 10:52:08 2011 -0700
     1.3 @@ -422,8 +422,7 @@
     1.4    assumes "\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f ----> a \<longrightarrow>
     1.5      eventually (\<lambda>n. P (f n)) sequentially"
     1.6    shows "eventually P (at a)"
     1.7 -  using assms sequentially_imp_eventually_within [where s=UNIV]
     1.8 -  unfolding within_UNIV by simp
     1.9 +  using assms sequentially_imp_eventually_within [where s=UNIV] by simp
    1.10  
    1.11  lemma LIMSEQ_SEQ_conv1:
    1.12    fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"