more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
header {* Plain HOL *}
theory Plain
imports Datatype 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