src/HOL/Plain.thy

added hint about writing "x : set xs".

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