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
webertj@17602
     1
(*  Title:      HOL/Main.thy
webertj@17602
     2
    ID:         $Id$
webertj@17602
     3
*)
wenzelm@9619
     4
wenzelm@12024
     5
header {* Main HOL *}
wenzelm@12024
     6
nipkow@15131
     7
theory Main
haftmann@24699
     8
imports Map
nipkow@15131
     9
begin
wenzelm@9650
    10
wenzelm@12024
    11
text {*
wenzelm@12024
    12
  Theory @{text Main} includes everything.  Note that theory @{text
wenzelm@12024
    13
  PreList} already includes most HOL theories.
wenzelm@19608
    14
*}
wenzelm@17395
    15
wenzelm@25223
    16
ML {* val HOL_proofs = ! Proofterm.proofs *}
wenzelm@23165
    17
haftmann@25964
    18
ML {* path_add "~~/src/HOL/Library" *}
haftmann@25964
    19
wenzelm@9650
    20
end