These lectures introduce theorem proving using the proof assistant Isabelle. Isabelle supports many logics, but by far the most popular is Higher Order Logic, the focus of these notes. Isabelle comes pre-packaged with its HOL libraries, as well as a proof editor (based on jEdit) and various other tools.

The proof developments shown in these notes are all developed with Isabelle 2024, but Isabelle 2025 (the latest version at time of writing) is largely backwards compatible with it. I have not upgraded due to some proof automation regressions in Isabelle 2025 that do not affect the content of these notes.