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)