Getting started
For getting started with Isabelle quickly, we recommend the Tutorial on Isabelle/HOL (in an earlier version published by Springer Verlag as LNCS 2283) and the course material.
Mailing lists and FAQ
You may use the user mailing list isabelle-users@cl.cam.ac.uk and its archive to discuss problems and results. Why not subscribe?
Please consult the FAQ for answers to frequent problems.
Advanced users may also profit from the developer mailing list isabelle-dev@in.tum.de. Subscribe.
Course material and exercises
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.
Project partners
Isabelle is a joint project between Larry Paulson (University of Cambridge, UK) and Tobias Nipkow (Technische Universität München, Germany).
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.
Isabelle in your neighborhood
Find out on the world map!
The Archive of Formal Proofs (AFP)
The Archive of Formal Proofs is 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.