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)
Prerequisites
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).