Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/HOL/Probability/Discrete_Topology.thy
changeset 50881 ae630bab13da
parent 50245 dea9363887a6
child 51000 c9adb50f74ad 
     1.1 --- a/src/HOL/Probability/Discrete_Topology.thy	Mon Jan 14 17:16:59 2013 +0100
     1.2 +++ b/src/HOL/Probability/Discrete_Topology.thy	Mon Jan 14 17:29:04 2013 +0100
     1.3 @@ -48,7 +48,7 @@
     1.4    thus "\<exists>f::'a discrete \<Rightarrow> nat. inj f" by blast
     1.5  qed
     1.6  
     1.7 -instance discrete :: (countable) countable_basis_space
     1.8 +instance discrete :: (countable) second_countable_topology
     1.9  proof
    1.10    let ?B = "(range (\<lambda>n::nat. {from_nat n::'a discrete}))"
    1.11    have "topological_basis ?B"
isabelle