* 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.
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
