# HG changeset patch
# User traytel
# Date 1385371225 -3600
# Node ID 9733ab5c1df6544523dce03d28544c0f09cb964a
# Parent  9387251b6a464db536084a063243fbc948deafe4
drop theorem duplicates

diff -r 9387251b6a46 -r 9733ab5c1df6 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Mon Nov 25 10:14:29 2013 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Mon Nov 25 10:20:25 2013 +0100
@@ -193,10 +193,6 @@
     by (auto simp add: infinite_nat_iff_unbounded)
 qed
 
-(* 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: "finite (UNIV::nat set) \<Longrightarrow> R"
   by simp
 
@@ -209,17 +205,6 @@
   then show False by simp
 qed
 
-(* duplicates Int.infinite_UNIV_int *)
-lemma int_infinite [simp]: "infinite (UNIV::int set)"
-proof -
-  from inj_int have "infinite (range int)"
-    by (rule range_inj_infinite)
-  moreover 
-  have "range int \<subseteq> (UNIV::int set)" by simp
-  ultimately show "infinite (UNIV::int set)"
-    by (simp add: infinite_super)
-qed
-
 text {*
   For any function with infinite domain and finite range there is some
   element that is the image of infinitely many domain elements.  In