John Harrison: tutorial on "The HOL Light Theorem Prover".

This will be a basic overview of a real-world theorem prover that has unusually simple foundations.