There are four important manuals distributed with the HOL system:
The Tutorial provides an introduction to the system for new users, as well as detailed installation instructions.
The Description provides a detailed description of all HOL's facilities, primarily targetting users, but also providing information about some of the core ML functions in the HOL API.
The Logic manual provides a detailed mathematical description of higher-order logic, as it is implemented in HOL. In particular, it demonstrates a model for the logic and its definitional principles in ZFC set theory.
The Reference provides a near-complete listing of the ML functions that implement the HOL system. These functions include user-level tactics and other tools, as well as entry-points that will probably be of most interest to people wishing to write their own tools.
Also, the Quick Reference Sheet provides a handy listing of core ML tactics and other user-level ML functions.
Some other documentation files are available.
tar-file
of a number of “sub”-manuals. These manuals document
some of the minor libraries within the system, and are mainly
out-of-date. Some users may find them useful nonetheless. (From
Kananaskis 4.)