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 redundant theorem attributes
authorhuffman
Sun, 07 Feb 2010 10:16:10 -0800
changeset 35056 d97b5c3af6d5
parent 35055 f0ecf952b864
child 35057 03d023236fcd
remove redundant theorem attributes
src/HOL/Library/Infinite_Set.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Infinite_Set.thy	Sun Feb 07 10:15:15 2010 -0800
+++ b/src/HOL/Library/Infinite_Set.thy	Sun Feb 07 10:16:10 2010 -0800
@@ -192,10 +192,11 @@
     by (auto simp add: infinite_nat_iff_unbounded)
 qed
 
-lemma nat_infinite [simp]: "infinite (UNIV :: nat set)"
+(* duplicates Finite_Set.infinite_UNIV_nat *)
+lemma nat_infinite: "infinite (UNIV :: nat set)"
   by (auto simp add: infinite_nat_iff_unbounded)
 
-lemma nat_not_finite [elim]: "finite (UNIV::nat set) \<Longrightarrow> R"
+lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
   by simp
 
 text {*
isabelle