Arto's Notes re: HOL4

HOL4 is a proof assistant for higher-order logic.

• https://hol-theorem-prover.org/
• https://github.com/HOL-Theorem-Prover/HOL