HOL Done Right
Unpublished draft, 21st August 1995.
In our opinion, history and compatibility considerations have rendered existing
HOL implementations rather messy and badly organized. We describe how, building
on joint work with Konrad Slind, we have produced a re-engineered HOL. Various
experiments have been tried on this `toy' version, and we will report the