--- 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