HOL Light proof advisor

sledgehammer の HOL Light 版
http://mws.cs.ru.nl/~urban/ha1.ogv (http://mws.cs.ru.nl/~urban/ha1.mp4)
http://mws.cs.ru.nl/~urban/2013-07-cicm.pdf
http://cl-informatik.uibk.ac.at/users/cek/docs/kaliszyk-cicm13.pdf