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 duplicate simp declaration
authorhuffman
Thu, 25 Aug 2011 11:56:20 -0700
changeset 44520 316256709a8c
parent 44519 ea85d78a994e
child 44521 083eedb37a37
remove duplicate simp declaration
src/HOL/Library/Extended_Real.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle