TY  - RPRT
TI  - Conversion of HOL Light proofs into Metamath
AU  - Mario Carneiro
PY  - 2015
UR  - https://arxiv.org/abs/1412.8091
ID  - 1412.8091
ER  -