Isabelle Tutorial at Bonn

A tutorial on Isabelle for students of mathematics will happen 03/04-Dec-2015 at Univ. Bonn (Workgroup of Prof. Koepke). The detailed schedule is available on the web page of Praktikum Mathematische Logik. The main language of the tutorial is German; materials are in English.

Notable topics

  • Isabelle/Pure as logical framework for Natural Deduction
  • Isabelle/Isar as proof language for formalized mathematics
  • Isabelle/ML as environment for developing tools for logic applications (including Prover IDE support)


The tutorial uses the following snapshot of the emerging winter release: Isabelle_01-Dec-2015.

Moreover, a full installation of LaTeX is required (Linux: TeX Live via package manager, Windows: MiKTeX, Mac OS X: MacTeX).