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