# HG changeset patch # User hoelzl # Date 1353491870 -3600 # Node ID 15523888c11bf090e74ae50a4502dd7b14af0731 # Parent 74773e3dc85db044a9968dbd0db9895ace92aed2 NEWS: document changes in HOL-Probability diff -r 74773e3dc85d -r 15523888c11b NEWS --- a/NEWS Wed Nov 21 10:48:58 2012 +0100 +++ b/NEWS Wed Nov 21 10:57:50 2012 +0100 @@ -198,6 +198,14 @@ * HOL/Cardinals: Theories of ordinals and cardinals (supersedes the AFP entry "Ordinals_and_Cardinals"). +* HOL/Probability: + - Add simproc "measurable" to automatically prove measurability + + - Add induction rules for sigma sets with disjoint union (sigma_sets_induct_disjoint) + and for Borel-measurable functions (borel_measurable_induct). + + - The Daniell-Kolmogorov theorem (the existence the limit of a projective family) + * Library/Countable_Set.thy: Theory of countable sets. * Library/Debug.thy and Library/Parallel.thy: debugging and parallel