Introduction

This document gives readers, with no experience in using HOL4, the most minimum knowledge needed to start using HOL4. The aim is to give a concise description of the basics in a format usable as a beginners' reference manual.

• Interaction with HOL4 (via emacs)
• Searching for theorems and theories
• Common proof tactics
• Further reading and general advice

The text assumes that the reader has HOL4 installed. You can download and install HOL4 following the instructions on https://hol-theorem-prover.org.