src/HOL/Main.thy
author haftmann
Sun May 06 21:49:26 2007 +0200 (2007-05-06)
changeset 22840 643bb625a2c3
parent 21254 d53f76357f41
child 23165 5d319b0f8bf9
permissions -rw-r--r--
minimal import
     1 (*  Title:      HOL/Main.thy
     2     ID:         $Id$
     3 *)
     4 
     5 header {* Main HOL *}
     6 
     7 theory Main
     8 imports Map Hilbert_Choice ATP_Linkup
     9 begin
    10 
    11 text {*
    12   Theory @{text Main} includes everything.  Note that theory @{text
    13   PreList} already includes most HOL theories.
    14 
    15   \medskip Late clause setup: installs \emph{all} known theorems
    16   into the clause cache; cf.\ theory @{text ATP_Linkup}.
    17 *}
    18 
    19 setup ResAxioms.setup
    20 
    21 end