src/HOL/Main.thy
author haftmann
Wed Sep 26 20:27:55 2007 +0200 (2007-09-26)
changeset 24728 e2b3a1065676
parent 24699 c6674504103f
child 24742 73b8b42a36b6
permissions -rw-r--r--
moved Finite_Set before Datatype
     1 (*  Title:      HOL/Main.thy
     2     ID:         $Id$
     3 *)
     4 
     5 header {* Main HOL *}
     6 
     7 theory Main
     8 imports Map
     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   FIXME: delete once @{text end_theory} actions are installed!
    18 *}
    19 
    20 setup ResAxioms.clause_cache_setup
    21 
    22 ML {* val HOL_proofs = !proofs *}
    23 
    24 end