NEWS;

tuned structure of Isabelle/HOL;

method setup for Classical steps;

tuned signature;

updated keywords;

moved (b)choice_iff(') to Hilbert_Choice

move theorems to be more generally useable

merged

made SML/NJ happy;

renamed prob_space to proj_prob_space as it clashed with Probability_Measure.prob_space

renamed measurable_compose -> measurable_finmap_compose, clashed with Sigma_Algebra.measurable_compose

measurability for nat_case and comb_seq

rules for AE and prob

rules for intergration: integrating nat-functions, integrals on finite measures, constant multiplication

more measurability rules

renamed to more appropriate lim_P for projective limit

allow arbitrary enumerations of basis in locale for generation of borel sets

repaired slip accidentally introduced in 57209cfbf16b

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;

removed some historic material that is obsolete or rarely used;

tuned;