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 List of all HOL4 base theories
- HOL4 Identifier Index List of all HOL4 identifiers
- HOL: Description Reference description of HOL4
- HOL Interaction (Emacs) HOL4 Emacs interaction guide
- HOL: Logic A formal description of HOL4 logic
- HOL Quick Reference Quick reference sheets for HOL4
- The HOL System Reference Comprehensive reference for the HOL4 system
- HOL: Tutorial 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