holbuild programming languages metatheory example This is an example project that uses holbuild to set up a failing HOL4 proof. To build the project after installing holbuild: holbuild build See this PDF for the background and tasks.