src/HOL/Main.thy
author haftmann
Fri Jan 25 14:53:58 2008 +0100 (2008-01-25)
changeset 25964 080f89d89990
parent 25223 7463251e7273
child 26729 43a72d892594
permissions -rw-r--r--
consistent interacitve bootstrap of HOL-Main
     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 
    16 ML {* val HOL_proofs = ! Proofterm.proofs *}
    17 
    18 ML {* path_add "~~/src/HOL/Library" *}
    19 
    20 end