# HG changeset patch
# User huffman
# Date 1314298580 25200
# Node ID 316256709a8c391189b588bf022511a6d7f44fda
# Parent  ea85d78a994eaf36abc0631309ea9b35e59e0869
remove duplicate simp declaration

diff -r ea85d78a994e -r 316256709a8c src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Aug 25 09:17:02 2011 -0700
+++ b/src/HOL/Library/Extended_Real.thy	Thu Aug 25 11:56:20 2011 -0700
@@ -2391,8 +2391,6 @@
   shows "limsup X \<le> limsup Y"
   using Limsup_mono[of X Y sequentially] eventually_sequentially assms by auto
 
-declare trivial_limit_sequentially[simp]
-
 lemma
   fixes X :: "nat \<Rightarrow> ereal"
   shows ereal_incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X"