src/HOL/Main.thy
author webertj
Fri Sep 23 16:01:45 2005 +0200 (2005-09-23)
changeset 17602 63367feba417
parent 17601 a6a322f96145
child 17618 1330157e156a
permissions -rw-r--r--
header (title/ID) added
     1 (*  Title:      HOL/Main.thy
     2     ID:         $Id$
     3 *)
     4 
     5 header {* Main HOL *}
     6 
     7 theory Main
     8 imports Refute Reconstruction
     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