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