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.