changeset 50881 | ae630bab13da |
parent 50245 | dea9363887a6 |
child 51000 | c9adb50f74ad |
--- a/src/HOL/Probability/Discrete_Topology.thy Mon Jan 14 17:16:59 2013 +0100 +++ b/src/HOL/Probability/Discrete_Topology.thy Mon Jan 14 17:29:04 2013 +0100 @@ -48,7 +48,7 @@ thus "\<exists>f::'a discrete \<Rightarrow> nat. inj f" by blast qed -instance discrete :: (countable) countable_basis_space +instance discrete :: (countable) second_countable_topology proof let ?B = "(range (\<lambda>n::nat. {from_nat n::'a discrete}))" have "topological_basis ?B"