Software needed

In the Interactive Theorem Proving course, the HOL theorem prover is used. For the practical part, you will need to have HOL installed. A description of what you need and how to install it can be found in Exercise 1.