src/HOL/Plain.thy

different session branches for HOL-Plain vs. Plain

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