These four lectures on *Getting Started With Isabelle* were delivered at the EEF Foundations School on Deduction and Theorem Proving. Edinburgh, Scotland (2000).

- Tour: a general overview of Isabelle
- Theory Files
- Interactive Proof
- The Mutilated Chess Board: an example

Lawrence C. Paulson • Computer Laboratory • University of Cambridge