eliminated markup for plain identifiers (frequent but insignificant);
reduced "black" markup (outer string etc. takes care of it already);
header {* Plain HOL *}
theory Plain
imports Datatype FunDef Extraction Metis
begin
text {*
Plain bootstrap of fundamental HOL tools and packages; does not
include @{text Hilbert_Choice}.
*}
end