adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
the code in "Nitpick_Preproc", which sorted the types using "typ_ord", was wrong and evil; it seems to have worked only because "*" was called "*"
header {* Plain HOL *}
theory Plain
imports Datatype Record FunDef Extraction
begin
text {*
Plain bootstrap of fundamental HOL tools and packages; does not
include @{text Hilbert_Choice}.
*}
ML {* path_add "~~/src/HOL/Library" *}
end