This is a hands-on tutorial introduction to the proof assistant
Isabelle/HOL. Slide presentations alternate with practical exercises:
partipants should bring their own laptop with Isabelle installed. The tutorial has three sections:
**Recursion and induction**

The initial introduction
concentrates on defining small functional programs and proving properties
about them by induction.
**Logic and Automation**

This section introduces more
of the logic and the available automation, including the famous
Sledgehammer that harnesses external automatic theorem provers.
**Structured proofs**

This section introduces
Isabelle's structured proof language Isar, which combines readability (via
block-structured natural-deduction proofs) with conciseness (via the rich
proof automation infrastructure).

The tutorial (given by Tobias Nipkow)
will be based on Part I of the book Concrete Semantics that is
freely availble online (and is also available as this separate
document).