Isabelle Repository for Relational and Algebraic Methods
This page contains some theory files for the theorem proving
environment Isabelle. Most of the theorems have been obtained by
automated reasoning with Isabelle's Sledgehammer tactics or by using
The files are still experimental and under constant revision and
extension. They contain so far more than 800 theorems.
The repository is open for everybody to use and contribute. It will
hopefully be replaced by some form of Wiki in the near future. If you
want to add theorems to the repository, please either send me a
formalised lemma with a Metis/SMT proof that compiles in the
respective file, or a handwritten theorem with a detailed manual
proof. Please understand that I currently cannot add theorems that
require major extensions to the theory files given.
Last changes: 22.01.2015