Patched version of HOL Light with tactic logging for machine learning purposes - View it on GitHub