Ramana Kumar: Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4. PxTP@CADE 2013: 110-116