"Premise Selection and External Provers for HOL4."

Thibault Gauthier, Cezary Kaliszyk (2015)
a service of Schloss Dagstuhl - Leibniz Center for Informatics