--- a/src/HOL/Library/Countable_Set.thy Tue Nov 27 11:29:47 2012 +0100
+++ b/src/HOL/Library/Countable_Set.thy Tue Nov 27 13:48:40 2012 +0100
@@ -235,6 +235,12 @@
by (auto dest: subset_range_from_nat_into countable_subset lists_mono)
qed
+lemma Collect_finite_eq_lists: "Collect finite = set ` lists UNIV"
+ using finite_list by auto
+
+lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\<Rightarrow>bool))"
+ by (simp add: Collect_finite_eq_lists)
+
subsection {* Misc lemmas *}
lemma countable_all: