[isabelle-dev] NEWS: new internal proof-producing SAT solver

[boehmes at in.tum.de]

* New internal SAT solver "dpll_p" that produces models and proof traces.

This refers to Isabelle/848d507584db. The added SAT solver should be more  
efficient than the internal SAT solvers "dpll" and "enumerate". Since the  
solver "dpll_p" produces proof traces, the tactics sat and satx can be  
applied to prove propositional goals without the need for quick_and_dirty.