# HG changeset patch
# User blanchet
# Date 1399222438 -7200
# Node ID 13a7bca533a3232fd39ab2f2556ae557771d4f25
# Parent  474767f0173ea51dea291967b2c939bf59d206cc
added 'satx' proof method to Try0

diff -r 474767f0173e -r 13a7bca533a3 NEWS
--- a/NEWS	Sun May 04 18:50:42 2014 +0200
+++ b/NEWS	Sun May 04 18:53:58 2014 +0200
@@ -352,7 +352,10 @@
 * New internal SAT solver "dpll_p" 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. Minor INCOMPATIBILITY.
+  use "dpll_p" instead. In addition, "dpll_p" 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.
 
 * SMT module:
   * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2
diff -r 474767f0173e -r 13a7bca533a3 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Sun May 04 18:50:42 2014 +0200
+++ b/src/HOL/Groebner_Basis.thy	Sun May 04 18:53:58 2014 +0200
@@ -86,9 +86,4 @@
 declare zmod_eq_dvd_iff[algebra]
 declare nat_mod_eq_iff[algebra]
 
-
-subsection {* Try0 *}
-
-ML_file "Tools/try0.ML"
-
 end
diff -r 474767f0173e -r 13a7bca533a3 src/HOL/Mutabelle/MutabelleExtra.thy
--- a/src/HOL/Mutabelle/MutabelleExtra.thy	Sun May 04 18:50:42 2014 +0200
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Sun May 04 18:53:58 2014 +0200
@@ -23,7 +23,7 @@
 quickcheck_params [quiet, finite_types = false, report = false, size = 5, iterations = 1000]
 
 (*
-nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
+nitpick_params [timeout = 5, sat_solver = MiniSat_JNI, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
 refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
 *)
 
diff -r 474767f0173e -r 13a7bca533a3 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Sun May 04 18:50:42 2014 +0200
+++ b/src/HOL/Presburger.thy	Sun May 04 18:53:58 2014 +0200
@@ -434,5 +434,9 @@
 lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
 lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
 
+
+subsection {* Try0 *}
+
+ML_file "Tools/try0.ML"
+
 end
-
diff -r 474767f0173e -r 13a7bca533a3 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Sun May 04 18:50:42 2014 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Sun May 04 18:53:58 2014 +0200
@@ -1032,4 +1032,3 @@
 in
   SatSolver.add_solver ("jerusat", jerusat)
 end;
-
diff -r 474767f0173e -r 13a7bca533a3 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Sun May 04 18:50:42 2014 +0200
+++ b/src/HOL/Tools/try0.ML	Sun May 04 18:53:58 2014 +0200
@@ -100,7 +100,8 @@
    ("fast", ((false, false), clas_attrs)),
    ("fastforce", ((false, false), full_attrs)),
    ("force", ((false, false), full_attrs)),
-   ("meson", ((false, false), metis_attrs))]
+   ("meson", ((false, false), metis_attrs)),
+   ("satx", ((false, false), no_attrs))];
 
 val apply_methods = map apply_named_method named_methods;