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. See also to the HOL4 cheatsheet.

Boolean expressions

Equalities

Quantifiers

Boolean connectives

Numbers

Records

Tactics on assumptions

Cases

Taming hol