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.

Andreas Linder (andili@kth.se) created a Docker container for HOL. It can be found on https://github.com/andreaslindner/HOL4docker. I myself am unable to help with getting it running, but Andreas can help if you want to use it and have trouble! Thanks Andreas!