src/HOL/Main.thy
author paulson
Thu Sep 27 17:55:28 2007 +0200 (2007-09-27)
changeset 24742 73b8b42a36b6
parent 24699 c6674504103f
child 25223 7463251e7273
permissions -rw-r--r--
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
theorems of Nat.thy are hidden by the Ordering.thy versions
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@23165
    16
ML {* val HOL_proofs = !proofs *}
wenzelm@23165
    17
wenzelm@9650
    18
end