--- a/NEWS Sun May 04 18:53:58 2014 +0200
+++ b/NEWS Sun May 04 18:57:45 2014 +0200
@@ -349,10 +349,10 @@
* Theory reorganizations:
* Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
-* New internal SAT solver "dpll_p" that produces models and proof traces.
+* New internal SAT solver "cdclite" that produces models and proof traces.
This solver replaces the internal SAT solvers "enumerate" and "dpll".
Applications that explicitly used one of these two SAT solvers should
- use "dpll_p" instead. In addition, "dpll_p" is now the default SAT
+ use "cdclite" instead. In addition, "cdclite" is now the default SAT
solver for the "sat" and "satx" proof methods and corresponding tactics;
the old default can be restored using
"declare [[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY.