Sources for the HOL Tutorial

Getting started

Make sure you:

• have HOL installed
• run Holmake in the mdbook-hol-filter directory

Then you can build the book using mdbook build in the root directory of this repo.

When working on the book, running mdbook serve can be nice.