My solutions for the KTH HOL4 course - Interactive Theorem Proving
- Link to the HOL4 webpage: https://hol-theorem-prover.org/
- Link to the course slides: https://hol-theorem-prover.org/hol-course.pdf
- Link to the exercise repository: https://gits-15.sys.kth.se/tuerk/ITP-exercises/
The slides, exercises and some files are proprietary content of Thomas Tuerk. I didn't
add the exercises PDF in this repository to be at peace with lawers, but I did add
some *Script.sml files for conveniance. Blah blah blah I don't own them blah blah
legal stuff blah blah blah please tell me if I did something wrong.
As for my source code and LaTeX documents, I purposedly didn't add any license notice, because I don't know how to simply add the license I want for both source code and LaTeX documents, and because these are solutions to exercises, so you're not supposed to work upon them. But you can find some inspiration and solutions to your problems if you're stuck :) Please contact me if you want to discuss anything (an Issue will do).