src/HOL/Main.thy
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 21254 d53f76357f41
child 22840 643bb625a2c3
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
     1 (*  Title:      HOL/Main.thy
     2     ID:         $Id$
     3 *)
     4 
     5 header {* Main HOL *}
     6 
     7 theory Main
     8 imports SAT 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 
    16 text {* \medskip Late clause setup: installs \emph{all} known theorems
    17   into the clause cache; cf.\ theory @{text ATP_Linkup}. *}
    18 
    19 setup ResAxioms.setup
    20 
    21 end