summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip

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