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