src/HOL/Main.thy
author webertj
Fri Sep 23 22:58:50 2005 +0200 (2005-09-23)
changeset 17618 1330157e156a
parent 17602 63367feba417
child 17721 b943c01e1c6d
permissions -rw-r--r--
new sat tactic imports resolution proofs from zChaff
     1 (*  Title:      HOL/Main.thy
     2     ID:         $Id$
     3 *)
     4 
     5 header {* Main HOL *}
     6 
     7 theory Main
     8 imports Refute Reconstruction SAT
     9 begin
    10 
    11 text {*
    12   Theory @{text Main} includes everything.  Note that theory @{text
    13   PreList} already includes most HOL theories.
    14 *}
    15 
    16 
    17 subsection {* Special hacks, late package setup etc. *}
    18 
    19 text {* \medskip Default values for refute, see also theory @{text
    20   Refute}.
    21 *}
    22 
    23 refute_params
    24  ["itself"=1,
    25   minsize=1,
    26   maxsize=8,
    27   maxvars=10000,
    28   maxtime=60,
    29   satsolver="auto"]
    30 
    31 
    32 text {* \medskip Clause setup: installs \emph{all} simprules and
    33   claset rules into the clause cache; cf.\ theory @{text
    34   Reconstruction}. *}
    35 
    36 setup ResAxioms.clause_setup
    37 
    38 end