# HG changeset patch
# User wenzelm
# Date 1128001845 -7200
# Node ID 8e098e040c2e6f805e2d5808bfeed4c9a3b7ec6c
# Parent  b943c01e1c6daf101ddfddf0ed43f3712af64ab5
explicit dependencies of SAT vs. Refute;
removed unused methods;

diff -r b943c01e1c6d -r 8e098e040c2e src/HOL/SAT.thy
--- a/src/HOL/SAT.thy	Thu Sep 29 15:50:44 2005 +0200
+++ b/src/HOL/SAT.thy	Thu Sep 29 15:50:45 2005 +0200
@@ -8,14 +8,26 @@
 
 header {* Reconstructing external resolution proofs for propositional logic *}
 
-theory SAT imports HOL
+theory SAT imports Refute
 
-uses (* "Tools/sat_solver.ML" -- already loaded by Refute.thy *)
+uses
      "Tools/cnf_funcs.ML"
      "Tools/sat_funcs.ML"
 
 begin
 
+text {* \medskip Late package setup: default values for refute, see
+  also theory @{text Refute}. *}
+
+refute_params
+ ["itself"=1,
+  minsize=1,
+  maxsize=8,
+  maxvars=10000,
+  maxtime=60,
+  satsolver="auto"]
+
+
 ML {* structure sat = SATFunc(structure cnf = cnf); *}
 
 method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
@@ -24,18 +36,4 @@
 method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
   "SAT solver (with definitional CNF)"
 
-(*
-method_setup cnf = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_tac) *}
-  "Transforming hypotheses in a goal into CNF"
-
-method_setup cnf_concl = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_concl_tac) *}
-  "Transforming the conclusion of a goal to CNF"
-
-method_setup cnf_thin = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_thin_tac) *}
-  "Same as cnf, but remove the original hypotheses"
-
-method_setup cnfx_thin = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnfx_thin_tac) *}
-  "Same as cnf_thin, but may introduce extra variables"
-*)
-
 end