Marktoberdorf 2011
Tobias Nipkow
and
Gerwin Klein
Lectures Nipkow: Isabelle/HOL
Demo theories:
Overview
Nat
List
Tree
Simp
Induct
Auto_Proof_Demo
Single_Step_Demo
Inductive_Demo
Isar_Demo
Isar_Induct_Demo
slides (long version)
lecture notes
Isar exercises
Isabelle download page
Lectures Klein: Semantics
Slides
Exercises
IMP theories (zip)