ISR 2017 
Formalizing Rewriting in Isabelle 


This Isabelle tutorial will cover the following topics. See also the short intro on slides. For each topic we will develop parts of the Isabelle theories live during the lectures, other parts will be provided as exercises where solutions will be made available shortly afterwards. The relevant Isabelle theories will be made available on this website and there will be regular updates.


In order to prepare for the course, each participant should install Isabelle and run it at least once.
  1. Download Isabelle 2016-1 and install it.
  2. Download a simple test theory and open it in Isabelle. The first start of Isabelle might take a while since it will start to compile the Isabelle theories for higher-order logic. The behavior of Isabelle should correspond to the following screenshot where in particular the quantifiers and the implications have nice symbols, and where the last proof is marked in red, indicating a non-accepted proof.
    screenshot of Isabelle
  3. Download the Archive of formal proofs. We will explain how to import this large collection of Isabelle formalizations within the course.

Isabelle theories

This archive contains the theory files related to this course.
Last update: 2017-07-07, 12:05