src/HOL/Library/Extended_Real.thy
changeset 44520 316256709a8c
parent 44170 510ac30f44c0
child 44669 8e6cdb9c00a7
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Thu Aug 25 09:17:02 2011 -0700
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Aug 25 11:56:20 2011 -0700
     1.3 @@ -2391,8 +2391,6 @@
     1.4    shows "limsup X \<le> limsup Y"
     1.5    using Limsup_mono[of X Y sequentially] eventually_sequentially assms by auto
     1.6  
     1.7 -declare trivial_limit_sequentially[simp]
     1.8 -
     1.9  lemma
    1.10    fixes X :: "nat \<Rightarrow> ereal"
    1.11    shows ereal_incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X"