src/HOL/Main.thy
author wenzelm
Sat Sep 17 18:11:21 2005 +0200 (2005-09-17)
changeset 17461 83f1dd9d901d
parent 17421 0382f6877b98
child 17509 054cd8972095
permissions -rw-r--r--
minor cleanup, moved stuff in its proper place;
     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 Hide the rather generic names used in theory @{text
    18   Commutative_Ring}. *}
    19 
    20 hide (open) const
    21   Pc Pinj PX
    22   Pol Add Sub Mul Pow Neg
    23   add mul neg sqr pow sub
    24   norm
    25 
    26 
    27 text {* \medskip Default values for rufute, see also theory @{text
    28   Refute}.
    29 *}
    30 
    31 refute_params
    32  ["itself"=1,
    33   minsize=1,
    34   maxsize=8,
    35   maxvars=10000,
    36   maxtime=60,
    37   satsolver="auto"]
    38 
    39 
    40 text {* \medskip Clause setup: installs \emph{all} simprules and
    41   claset rules into the clause cache; cf.\ theory @{text
    42   Reconstruction}. *}
    43 
    44 setup ResAxioms.clause_setup
    45 
    46 end