explicit dependencies of SAT vs. Refute;
moved late refute setup to SAT;

--- a/src/HOL/Main.thy	Thu Sep 29 15:50:43 2005 +0200
+++ b/src/HOL/Main.thy	Thu Sep 29 15:50:44 2005 +0200
@@ -5,7 +5,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Refute Reconstruction SAT
+imports SAT Reconstruction
 begin
 
 text {*
@@ -14,22 +14,7 @@
 *}
 
 
-subsection {* Special hacks, late package setup etc. *}
-
-text {* \medskip Default values for refute, see also theory @{text
-  Refute}.
-*}
-
-refute_params
- ["itself"=1,
-  minsize=1,
-  maxsize=8,
-  maxvars=10000,
-  maxtime=60,
-  satsolver="auto"]
-
-
-text {* \medskip Clause setup: installs \emph{all} simprules and
+text {* \medskip Late clause setup: installs \emph{all} simprules and
   claset rules into the clause cache; cf.\ theory @{text
   Reconstruction}. *}
 

--- a/src/HOL/Refute.thy	Thu Sep 29 15:50:43 2005 +0200
+++ b/src/HOL/Refute.thy	Thu Sep 29 15:50:44 2005 +0200
@@ -78,7 +78,7 @@
 (*                       This value is ignored under some ML compilers.      *)
 (* "satsolver"   string  Name of the SAT solver to be used.                  *)
 (*                                                                           *)
-(* See 'HOL/Main.thy' for default values.                                    *)
+(* See 'HOL/SAT.thy' for default values.                                     *)
 (*                                                                           *)
 (* The size of particular types can be specified in the form type=size       *)
 (* (where 'type' is a string, and 'size' is an int).  Examples:              *)
@@ -97,7 +97,7 @@
 (*                            syntax                                         *)
 (* HOL/Refute.thy             This file: loads the ML files, basic setup,    *)
 (*                            documentation                                  *)
-(* HOL/Main.thy               Sets default parameters                        *)
+(* HOL/SAT.thy                Sets default parameters                        *)
 (* HOL/ex/RefuteExamples.thy  Examples                                       *)
 (* ------------------------------------------------------------------------- *)
 \end{verbatim}