Introduction to HOL : a theorem proving environment for higher order logic - Gordon, M.J.C; Melham, T.F (Cambridge University Press, 1993)