Isabelle at Edinburgh

Welcome to Isabelle at Edinburgh!

Isabelle is a generic theorem prover, developed at the University of Cambridge. New logics are introduced by specifying their syntax and rules of inference; proof procedures can be expressed using tactics and tacticals.

Isabelle has four manuals:

• Introduction to Isabelle
• Isabelle Reference Manual
• Isabelle Logics Manual
• Isabelle System Manual

There are some more technical details in:

• Axiomatic Type Classes
• (Co)Inductive Definitions in ZF

Here are some tutorial documents for beginners:

• Tutorial on Isabelle/HOL (DRAFT; part of upcoming release of Isabelle)
• Gentle Introduction to Isabelle by Sara Kalvala

You can find out about the theory structure of the standard logics on the logics page maintained at Munich.

At Edinburgh, David Aspinall has developed an interface for Isabelle, Isamode, based on XEmacs.
David Aspinall and others have developed another Emacs interface for Isabelle and other theorem provers, called Proof General.

There are some local instructions for using Isabelle at Edinburgh, or if you are reading this remotely, here's where you can ftp Isabelle from in Cambridge.

More documentations and papers related to Isabelle can be found at Cambridge.

Please send any queries, problems or suggestions to isabelle@dcs.ed.ac.uk