(* 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