HOL4 Documentation

This page collects the HOL4 documentation I use for the trindemossen-2 version. The links below point to the pinned reference set for that release, so you can open any guide in a new tab and use this page as a central starting point.

HOL4 Theory Index HTML: List of all HOL4 base theories.
HOL4 Identifier Index HTML: List of all HOL4 identifiers.
HOL: Description PDF: Reference description of HOL4.
HOL Interaction (Emacs) PDF: HOL4 Emacs interaction guide.
HOL: Logic PDF: A formal description of HOL4 logic.
HOL Quick Reference PDF: Quick reference sheets for HOL4.
The HOL System Reference PDF: Comprehensive reference for the HOL4 system.
HOL: Tutorial PDF: Step-by-step tutorial for HOL4.

For general information, visit the HOL4 official website.

Official documentation is also available at https://hol-theorem-prover.org/docs/trindemossen-2/

Source repository: HOL-Theorem-Prover/HOL