src/HOL/Plain.thy

added props_text (from isar_syn.ML);

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