src/HOL/Plain.thy
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 27368 9f90ac19e32b
child 29304 5c71a6da989d
permissions -rw-r--r--
moved global ML bindings to global place;
     1 (*  Title:      HOL/Plain.thy
     2     ID:         $Id$
     3 
     4 Contains fundamental HOL tools and packages.  Does not include Hilbert_Choice.
     5 *)
     6 
     7 header {* Plain HOL *}
     8 
     9 theory Plain
    10 imports Datatype FunDef Record SAT Extraction
    11 begin
    12 
    13 ML {* path_add "~~/src/HOL/Library" *}
    14 
    15 end