changeset 27368 | 9f90ac19e32b |
child 29304 | 5c71a6da989d |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Plain.thy Thu Jun 26 10:07:01 2008 +0200 @@ -0,0 +1,15 @@ +(* Title: HOL/Plain.thy + ID: $Id$ + +Contains fundamental HOL tools and packages. Does not include Hilbert_Choice. +*) + +header {* Plain HOL *} + +theory Plain +imports Datatype FunDef Record SAT Extraction +begin + +ML {* path_add "~~/src/HOL/Library" *} + +end