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. For this you need.¶ ¶ Standard ML You will need to have standard ML available. Please install PolyML 5.6 or later (download,webpage).¶ ¶ HOL Please install a recent version of the HOL theorem prover. I recomment installing the most recent version from the git repository. If for some reason you don't want to do this, the latest release should be fine as well. Installation instructions can be found on HOL's webpage.¶ ¶ Emacs In the lecture emacs will be used as a user/interface. Please install a recent version of Emacs. Activate the hol-mode. For details how to do it, please look at it's documentation.¶ ¶ SML mode To enable syntax highlighting for ML, please install the SML mode.¶ ¶ If you have questions, please contact Thomas TuerkA description of what you need and how to install it can be found in Exercise 1.