NEWS
changeset 56815 848d507584db
parent 56807 ab36ec0c8eb5
child 56826 ba18bd41e510
child 56838 477cd67f963f
     1.1 --- a/NEWS	Thu May 01 22:41:03 2014 +0200
     1.2 +++ b/NEWS	Thu May 01 22:56:59 2014 +0200
     1.3 @@ -341,6 +341,8 @@
     1.4  * Theory reorganizations:
     1.5    * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
     1.6  
     1.7 +* New internal SAT solver "dpll_p" that produces models and proof traces.
     1.8 +
     1.9  * SMT module:
    1.10    * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2
    1.11      and supports recent versions of Z3 (e.g., 4.3). The new proof method is