src/HOL/Probability/Regularity.thy
2012-11-19 ago tuned: use induction rule sigma_sets_induct_disjoint
2012-11-15 ago generalized to copy of countable types instead of instantiation of nat for discrete topology
2012-11-15 ago regularity of measures, therefore: