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 ***