src/HOL/Probability/Discrete_Topology.thy
2016-01-08 hoelzl 2016-01-08 add uniform spaces
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2013-03-05 hoelzl 2013-03-05 use generate_topology for second countable topologies, does not require intersection stable basis
2013-01-31 hoelzl 2013-01-31 use order topology for extended reals
2013-01-14 hoelzl 2013-01-14 renamed countable_basis_space to second_countable_topology
2012-11-27 immler 2012-11-27 based countable topological basis on Countable_Set
2012-11-15 immler 2012-11-15 generalized to copy of countable types instead of instantiation of nat for discrete topology