# HG changeset patch
# User blanchet
# Date 1399222242 -7200
# Node ID 474767f0173ea51dea291967b2c939bf59d206cc
# Parent  67e6803e3765d2b12dbe8e07f18d9faffbf58cfa
make 'dpll_p' the default SAT solver, rather than the hard-to-get zChaff-with-proofs

diff -r 67e6803e3765 -r 474767f0173e src/HOL/Tools/sat.ML
--- a/src/HOL/Tools/sat.ML	Sun May 04 18:14:59 2014 +0200
+++ b/src/HOL/Tools/sat.ML	Sun May 04 18:50:42 2014 +0200
@@ -65,7 +65,7 @@
 fun cond_tracing ctxt msg =
   if Config.get ctxt trace then tracing (msg ()) else ();
 
-val solver = Attrib.setup_config_string @{binding sat_solver} (K "zchaff_with_proofs");
+val solver = Attrib.setup_config_string @{binding sat_solver} (K "dpll_p");
   (*see HOL/Tools/sat_solver.ML for possible values*)
 
 val counter = Unsynchronized.ref 0;