HOL4 tactics and tips & tricks

In the following we document tactics and tips & tricks for the HOL4 theorem prover. Some of those are extracted from discussions on the CakeML Slack, some are found in code and some are own work.

Boolean expressions

Equalities

Quantifiers

Boolean connectives

Tactics on assumptions

Cases

Taming hol