If you have a question about this talk, please contact Thomas Tuerk.
In this talk, I will expose various problems in using existing HOL theorem provers, and advocate the use of a new proof-checker for HOL that is carefully designed to avoid these problems.