As requested by @konrad-slind. These features of HOL4 have not had their correctness/soundness argument properly checked.