src/HOL/Main.thy
author wenzelm
Mon Oct 29 16:13:41 2007 +0100 (2007-10-29)
changeset 25223 7463251e7273
parent 24742 73b8b42a36b6
child 25964 080f89d89990
permissions -rw-r--r--
qualified Proofterm.proofs;
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
wenzelm@9650
    18
end