Consts.eq_const is back again (cf. 907da436f8a9) -- required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;
header {* Plain HOL *}
theory Plain
imports Datatype FunDef Record Extraction Divides
begin
text {*
Plain bootstrap of fundamental HOL tools and packages; does not
include @{text Hilbert_Choice}.
*}
ML {* path_add "~~/src/HOL/Library" *}
end