src/HOL/Probability/Borel_Space.thy

     ultimately show "(x, y) \<in> (\<Union>(a, b)\<in>{X \<in> A \<times> B. fst X \<times> snd X \<subseteq> S}. a \<times> b)"
       by (intro UN_I[of "(A0, B0)"]) auto
   qed auto
 qed (metis A B topological_basis_open open_Times)
 
-instance prod :: (countable_basis_space, countable_basis_space) countable_basis_space
+instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology
 proof
   obtain A :: "'a set set" where "countable A" "topological_basis A"
     using ex_countable_basis by auto
   moreover
   obtain B :: "'b set set" where "countable B" "topological_basis B"

   ultimately show "\<exists>B::('a \<times> 'b) set set. countable B \<and> topological_basis B"
     by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod)
 qed
 
 lemma borel_measurable_Pair[measurable (raw)]:
-  fixes f :: "'a \<Rightarrow> 'b::countable_basis_space" and g :: "'a \<Rightarrow> 'c::countable_basis_space"
+  fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
   assumes f[measurable]: "f \<in> borel_measurable M"
   assumes g[measurable]: "g \<in> borel_measurable M"
   shows "(\<lambda>x. (f x, g x)) \<in> borel_measurable M"
 proof (subst borel_eq_countable_basis)
   let ?B = "SOME B::'b set set. countable B \<and> topological_basis B"

     using closed_vimage_snd
     by (auto simp: continuous_on_closed closed_closedin vimage_def)
 qed
 
 lemma borel_measurable_continuous_Pair:
-  fixes f :: "'a \<Rightarrow> 'b::countable_basis_space" and g :: "'a \<Rightarrow> 'c::countable_basis_space"
+  fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
   assumes [measurable]: "f \<in> borel_measurable M"
   assumes [measurable]: "g \<in> borel_measurable M"
   assumes H: "continuous_on UNIV (\<lambda>x. H (fst x) (snd x))"
   shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M"
 proof -

 qed
 
 section "Borel spaces on euclidean spaces"
 
 lemma borel_measurable_inner[measurable (raw)]:
-  fixes f g :: "'a \<Rightarrow> 'b::{countable_basis_space, real_inner}"
+  fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_inner}"
   assumes "f \<in> borel_measurable M"
   assumes "g \<in> borel_measurable M"
   shows "(\<lambda>x. f x \<bullet> g x) \<in> borel_measurable M"
   using assms
   by (rule borel_measurable_continuous_Pair)