src/HOL/Plain.thy
author haftmann
Thu Jun 26 10:07:01 2008 +0200 (2008-06-26)
changeset 27368 9f90ac19e32b
child 29304 5c71a6da989d
permissions -rw-r--r--
established Plain theory and image
haftmann@27368
     1
(*  Title:      HOL/Plain.thy
haftmann@27368
     2
    ID:         $Id$
haftmann@27368
     3
haftmann@27368
     4
Contains fundamental HOL tools and packages.  Does not include Hilbert_Choice.
haftmann@27368
     5
*)
haftmann@27368
     6
haftmann@27368
     7
header {* Plain HOL *}
haftmann@27368
     8
haftmann@27368
     9
theory Plain
haftmann@27368
    10
imports Datatype FunDef Record SAT Extraction
haftmann@27368
    11
begin
haftmann@27368
    12
haftmann@27368
    13
ML {* path_add "~~/src/HOL/Library" *}
haftmann@27368
    14
haftmann@27368
    15
end