src/HOL/Main.thy
author haftmann
Tue May 09 14:18:40 2006 +0200 (2006-05-09)
changeset 19607 07eeb832f28d
parent 18510 0a6c24f549c3
child 19608 81fe44909dd5
permissions -rw-r--r--
introduced characters for code generator; some improved code lemmas for some list functions
     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 text {* \medskip Late clause setup: installs \emph{all} simprules and
    16   claset rules into the clause cache; cf.\ theory @{text
    17   Reconstruction}. *}
    18 
    19 setup ResAxioms.setup
    20 
    21 end