src/HOL/Main.thy
author wenzelm
Tue Sep 20 14:03:38 2005 +0200 (2005-09-20)
changeset 17509 054cd8972095
parent 17461 83f1dd9d901d
child 17601 a6a322f96145
permissions -rw-r--r--
removed Commutative_Ring hacks;
     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 rufute, 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