# 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