src/HOL/Main.thy
changeset 17721 b943c01e1c6d
parent 17618 1330157e156a
child 17905 1574533861b1
     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