Conversion of HOL Light proofs into Metamath

Mario M. Carneiro. Conversion of HOL Light proofs into Metamath. J. Formalized Reasoning, 9(1):187-200, 2016. [doi]

Abstract

Abstract is missing.