Introduction to HOL
A theorem proving environment for higher order logic
Edited by M. J. C. Gordon and T. F. Melham
University Press, 1993.
The book is an edited version of a combination of the HOL tutorial and system description, published in a format suitable for convenient reference at the terminal as well as reading. The purpose of this volume was to provide a coherent and self-contained introduction to HOL and to extract and compress from various sources most of the material needed for day-to-day work with the system.
After a quick overview that gives a hands-on feel for the way HOL is used, there follows a detailed description of the HOL meta-language ML. Part III then presents the logic that HOL supports. Part IV describes how HOL is embedded in ML, and Part V then explains the theorem-proving infrastructure provided by HOL. Finally, two appendices contain a subset of the reference manual and a survey of the HOL libraries, including an example of the documentation for an actual HOL library.
All royalties from this book go into a fund to support the HOL system and HOL-based activities.
You and read a review by Graham Hutton in the Journal of Functional Programming, 4(4):557-559, 1994.