HOL4 Documentation

Documentation for the HOL4 theorem prover.

Getting started

New to HOL? Start with the Tutorial for a step-by-step introduction through worked examples, then keep these handy:

HOL: Description
Reference description of the HOL system: the kernel, the libraries, and the theories distributed with HOL.
HOL: Tutorial
Step-by-step introduction to HOL through worked examples.
HOL: Quick Reference
A compact summary of the tactics, rules, conversions, and support functions used most often in day-to-day HOL4 proof, with links into the Reference manual.
HOL: Reference
Per-entry reference for every HOL function, theorem, tactic, conversion, and theory.
HOL: Interaction (emacs)
Driving HOL from Emacs: hol-mode keystrokes, goal navigation, theorem search, common proof tactics, and the editor side of the proof workflow.
HOL: Logic
A formal description of the higher order logic implemented by the HOL system, with its set-theoretic semantics.
HOL: Developers
Documentation for developing HOL4 itself: building and configuring the system, and assorted internals.