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

  1. Tour: a general overview of Isabelle
  2. Theory Files
  3. Interactive Proof
  4. The Mutilated Chess Board: an example
Lawrence C. Paulson • Computer Laboratory • University of Cambridge