prefer implementation in HOL;
n.b. code_reflect cannot reflect type synonyms

corrected headers

hide constants of auxiliary type finmap

generalized to copy of countable types instead of instantiation of nat for discrete topology

added projective limit;
proof is based on auxiliary type finmap::polish_space

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

tuned -- eliminated obsolete citation of isabelle-ref;

updated basic equality rules;

removed somewhat pointless historic material;

updated unification options;