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 SMT solvers.
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