src/HOL/Main.thy
author wenzelm
Thu May 31 18:16:54 2007 +0200 (2007-05-31)
changeset 23165 5d319b0f8bf9
parent 22840 643bb625a2c3
child 24632 779fc4fcbf8b
permissions -rw-r--r--
HOL_proofs;
     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 ML {* val HOL_proofs = !proofs *}
    22 
    23 end