# HG changeset patch
# User paulson
# Date 1170333679 -3600
# Node ID 699385e6cb45b0e8c73aedb1ddafe06b36a1e93d
# Parent  30ab97554602edcb9b5222442adb713a0780ddb9
new theorem int_infinite

diff -r 30ab97554602 -r 699385e6cb45 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Wed Jan 31 20:07:40 2007 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Thu Feb 01 13:41:19 2007 +0100
@@ -215,6 +215,15 @@
   then show False by simp
 qed
 
+lemma int_infinite [simp]:
+  shows "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 {*
   The ``only if'' direction is harder because it requires the
   construction of a sequence of pairwise different elements of an