NEWS

--- a/NEWS	Thu May 01 22:41:03 2014 +0200
+++ b/NEWS	Thu May 01 22:56:59 2014 +0200
@@ -341,6 +341,8 @@
 * Theory reorganizations:
   * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
 
+* New internal SAT solver "dpll_p" that produces models and proof traces.
+
 * SMT module:
   * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2
     and supports recent versions of Z3 (e.g., 4.3). The new proof method is