src/HOL/Main.thy
author paulson
Fri Dec 23 17:37:54 2005 +0100 (2005-12-23)
changeset 18510 0a6c24f549c3
parent 18315 e52f867ab851
child 19607 07eeb832f28d
permissions -rw-r--r--
the "skolem" attribute and better initialization of the clause database
     1 (*  Title:      HOL/Main.thy
     2     ID:         $Id$
     3 *)
     4 
     5 header {* Main HOL *}
     6 
     7 theory Main
     8 imports SAT Reconstruction ResAtpMethods
     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 text {* \medskip Late clause setup: installs \emph{all} simprules and
    18   claset rules into the clause cache; cf.\ theory @{text
    19   Reconstruction}. *}
    20 
    21 setup ResAxioms.setup
    22 
    23 end