HOL Documentation

There are four important manuals distributed with the HOL system:

Tutorial (in Italian)

The Tutorial provides an introduction to the system for new users, as well as detailed installation instructions.

Description

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.

Logic (in Italian)

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.

Reference

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.


Time-stamp: "Monday, 10 November 2014; 05:22 UTC (Michael Norrish)"