Main Page

This is the community wiki for Isabelle.

Isabelle is developed at University of Cambridge (Larry Paulson), TU München (Tobias Nipkow), and Augsburg (Makarius Wenzel). Isabelle's maintainer is Makarius Wenzel.

Both sites employ numerous activities around Isabelle; for details, have a look at the local websites in Cambridge and Munich; there is also an (incomplete) list of past and present projects undertaken using Isabelle.

You need an account to add or change something in this wiki.

Getting started

For getting started with Isabelle quickly:

• Introduction to Programming and Proving in Isabelle/HOL
• Tutorial on Isabelle/HOL
  (earlier version published by Springer Verlag as LNCS 2283)
• Course Material
  The course material page makes slides, demos, and exercises of a growing number of Isabelle courses available. It is meant as a resource for people who would like to learn Isabelle as well as for those who would like to teach it.
• Frequently asked questions
• Getting Started with Isabelle/jEdit
• The Isabelle Cookbook
  A tutorial for programming on the ML-level of Isabelle

Mailing Lists

• User mailing list isabelle-users@cl.cam.ac.uk [Subscribe] [official, gmane.org]
• Development mailing list isabelle-dev@in.tum.de [Subscribe] [official, mail-archive.com, gmane.org]
  When referring to a problem with the Isabelle repository always provide the Mercurial changeset. It can be looked up with hg id.

Finding Answers for your Questions on StackOverflow

Several Isabelle community members are active on StackOverflow, a web platform where you can ask questions about concrete problems.

Tips and Tricks

• Generate TeX Snippets
• Extending Isabelle/jEdit
• Searching for Theorems
• Notes on Isabelle/HOL Simprocs
• Lemma Collections
• Confusing Isabelle error messages
• Isabelle Cheat Sheet

Isabelle Extensions

• AFP: The Archive of Formal Proofs
  A collection of proof libraries, examples, and larger scientific developments, mechanically checked in Isabelle. It is organized in the way of a scientific journal. Submissions are refereed.
• Add-on tools for Isabelle
• Collections of Isabelle theories

Isabelle Development HOWTOs

• Working with the repository version of Isabelle
• Publish contributions as an external
• Building AFP
• Other Work in Progress

Isabelle Administration HOWTOs

• Administration of the mira testing facilities
• Administration of the isatest facilities
• Reconstructing the Isabelle repository

Collections of miscellaneous notes

• How to use this wiki
• Ideas for simp trace
• Notes on Isar keywords
• Isabelle in your neighbourhood: The Isabelle worldmap

---

• List of all pages

Technical information for using this wiki is found in the user manual.