src/HOL/Library/Infinite_Set.thy
changeset 35056 d97b5c3af6d5
parent 34941 156925dd67af
child 35844 65258d2c3214
     1.1 --- a/src/HOL/Library/Infinite_Set.thy	Sun Feb 07 10:15:15 2010 -0800
     1.2 +++ b/src/HOL/Library/Infinite_Set.thy	Sun Feb 07 10:16:10 2010 -0800
     1.3 @@ -192,10 +192,11 @@
     1.4      by (auto simp add: infinite_nat_iff_unbounded)
     1.5  qed
     1.6  
     1.7 -lemma nat_infinite [simp]: "infinite (UNIV :: nat set)"
     1.8 +(* duplicates Finite_Set.infinite_UNIV_nat *)
     1.9 +lemma nat_infinite: "infinite (UNIV :: nat set)"
    1.10    by (auto simp add: infinite_nat_iff_unbounded)
    1.11  
    1.12 -lemma nat_not_finite [elim]: "finite (UNIV::nat set) \<Longrightarrow> R"
    1.13 +lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
    1.14    by simp
    1.15  
    1.16  text {*