src/HOL/Probability/Regularity.thy
2013-05-25 haftmann 2013-05-25 weaker precendence of syntax for big intersection and union on sets
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-12-14 wenzelm 2012-12-14 updated some headers;
2012-11-27 immler 2012-11-27 based countable topological basis on Countable_Set
2012-11-27 immler 2012-11-27 qualified interpretation of sigma_algebra, to avoid name clashes
2012-11-19 hoelzl 2012-11-19 tuned: use induction rule sigma_sets_induct_disjoint
2012-11-15 immler 2012-11-15 generalized to copy of countable types instead of instantiation of nat for discrete topology
2012-11-15 immler 2012-11-15 regularity of measures, therefore: characterization of closure with infimum distance; characterize of compact sets as totally bounded; added Diagonal_Subsequence to Library; introduced (enumerable) topological basis; rational boxes as basis of ordered euclidean space; moved some lemmas upwards