[ Isabelle logo ]

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:

There are some more technical details in: Here are some tutorial documents for beginners: 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

David Aspinall <da@dcs.ed.ac.uk>
Last modified: Fri Jan 15 14:52:58 GMT 1999