src/HOL/Library/Countable_Set.thy

--- a/src/HOL/Library/Countable_Set.thy	Mon Oct 03 14:09:26 2016 +0100
+++ b/src/HOL/Library/Countable_Set.thy	Fri Sep 30 16:08:38 2016 +0200
@@ -284,6 +284,9 @@
 lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\<Rightarrow>bool))"
   by (simp add: Collect_finite_eq_lists)
 
+lemma countable_int: "countable \<int>"
+  unfolding Ints_def by auto
+
 lemma countable_rat: "countable \<rat>"
   unfolding Rats_def by auto