1.1 --- a/src/HOL/Library/Countable_Set.thy	Thu Jan 17 11:57:17 2013 +0100
     1.2 +++ b/src/HOL/Library/Countable_Set.thy	Thu Jan 17 11:59:12 2013 +0100
     1.3 @@ -241,6 +241,16 @@
     1.4  lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\<Rightarrow>bool))"
     1.5    by (simp add: Collect_finite_eq_lists)
     1.6  
     1.7 +lemma countable_rat: "countable \<rat>"
     1.8 +  unfolding Rats_def by auto
     1.9 +
    1.10 +lemma Collect_finite_subset_eq_lists: "{A. finite A \<and> A \<subseteq> T} = set ` lists T"
    1.11 +  using finite_list by (auto simp: lists_eq_set)
    1.12 +
    1.13 +lemma countable_Collect_finite_subset:
    1.14 +  "countable T \<Longrightarrow> countable {A. finite A \<and> A \<subseteq> T}"
    1.15 +  unfolding Collect_finite_subset_eq_lists by auto
    1.16 +
    1.17  subsection {* Misc lemmas *}
    1.18  
    1.19  lemma countable_all:

     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 11:57:17 2013 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 11:59:12 2013 +0100
     2.3 @@ -21,9 +21,6 @@
     2.4    "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"
     2.5    by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
     2.6  
     2.7 -lemma countable_rat: "countable \<rat>"
     2.8 -  unfolding Rats_def by auto
     2.9 -
    2.10  subsection {* Topological Basis *}
    2.11  
    2.12  context topological_space