explicit dependencies of SAT vs. Refute;
authorwenzelm
Thu Sep 29 15:50:44 2005 +0200 (2005-09-29)
changeset 17721b943c01e1c6d
parent 17720 da9199e6b674
child 17722 8e098e040c2e
explicit dependencies of SAT vs. Refute;
moved late refute setup to SAT;
src/HOL/Main.thy
src/HOL/Refute.thy
     1.1 --- a/src/HOL/Main.thy	Thu Sep 29 15:50:43 2005 +0200
     1.2 +++ b/src/HOL/Main.thy	Thu Sep 29 15:50:44 2005 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Main HOL *}
     1.5  
     1.6  theory Main
     1.7 -imports Refute Reconstruction SAT
     1.8 +imports SAT Reconstruction
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -14,22 +14,7 @@
    1.13  *}
    1.14  
    1.15  
    1.16 -subsection {* Special hacks, late package setup etc. *}
    1.17 -
    1.18 -text {* \medskip Default values for refute, see also theory @{text
    1.19 -  Refute}.
    1.20 -*}
    1.21 -
    1.22 -refute_params
    1.23 - ["itself"=1,
    1.24 -  minsize=1,
    1.25 -  maxsize=8,
    1.26 -  maxvars=10000,
    1.27 -  maxtime=60,
    1.28 -  satsolver="auto"]
    1.29 -
    1.30 -
    1.31 -text {* \medskip Clause setup: installs \emph{all} simprules and
    1.32 +text {* \medskip Late clause setup: installs \emph{all} simprules and
    1.33    claset rules into the clause cache; cf.\ theory @{text
    1.34    Reconstruction}. *}
    1.35  
     2.1 --- a/src/HOL/Refute.thy	Thu Sep 29 15:50:43 2005 +0200
     2.2 +++ b/src/HOL/Refute.thy	Thu Sep 29 15:50:44 2005 +0200
     2.3 @@ -78,7 +78,7 @@
     2.4  (*                       This value is ignored under some ML compilers.      *)
     2.5  (* "satsolver"   string  Name of the SAT solver to be used.                  *)
     2.6  (*                                                                           *)
     2.7 -(* See 'HOL/Main.thy' for default values.                                    *)
     2.8 +(* See 'HOL/SAT.thy' for default values.                                     *)
     2.9  (*                                                                           *)
    2.10  (* The size of particular types can be specified in the form type=size       *)
    2.11  (* (where 'type' is a string, and 'size' is an int).  Examples:              *)
    2.12 @@ -97,7 +97,7 @@
    2.13  (*                            syntax                                         *)
    2.14  (* HOL/Refute.thy             This file: loads the ML files, basic setup,    *)
    2.15  (*                            documentation                                  *)
    2.16 -(* HOL/Main.thy               Sets default parameters                        *)
    2.17 +(* HOL/SAT.thy                Sets default parameters                        *)
    2.18  (* HOL/ex/RefuteExamples.thy  Examples                                       *)
    2.19  (* ------------------------------------------------------------------------- *)
    2.20  \end{verbatim}