src/HOL/Plain.thy
author wenzelm
Fri Jan 02 00:21:59 2009 +0100 (2009-01-02)
changeset 29304 5c71a6da989d
parent 27368 9f90ac19e32b
child 29609 a010aab5bed0
permissions -rw-r--r--
tuned header and description of boot files;
haftmann@27368
     1
header {* Plain HOL *}
haftmann@27368
     2
haftmann@27368
     3
theory Plain
haftmann@27368
     4
imports Datatype FunDef Record SAT Extraction
haftmann@27368
     5
begin
haftmann@27368
     6
wenzelm@29304
     7
text {*
wenzelm@29304
     8
  Plain bootstrap of fundamental HOL tools and packages; does not
wenzelm@29304
     9
  include @{text Hilbert_Choice}.
wenzelm@29304
    10
*}
wenzelm@29304
    11
haftmann@27368
    12
ML {* path_add "~~/src/HOL/Library" *}
haftmann@27368
    13
haftmann@27368
    14
end