# HG changeset patch
# User hoelzl
# Date 1421175708 -3600
# Node ID 546fbee3123ee828a8b61436073561f02e8e6505
# Parent  f0707dc3d9aaa1757e33a72243ccedb31a6ac9ae
NEWS

diff -r f0707dc3d9aa -r 546fbee3123e NEWS
--- a/NEWS	Tue Jan 13 19:10:36 2015 +0100
+++ b/NEWS	Tue Jan 13 20:01:48 2015 +0100
@@ -196,6 +196,10 @@
     See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for
     examples.
 
+* HOL-Probability: Reworked measurability prover
+  - applies destructor rules repeatetly
+  - removed application splitting (replaced by destructor rule)
+  - added congruence rules to rewrite measure spaces under the sets projection
 
 *** Document preparation ***