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:
You can find out about the theory structure of the standard logics on the logics page maintained at Munich.
- Tutorial on Isabelle/HOL (DRAFT; part of upcoming release of Isabelle)
- Gentle Introduction to Isabelle by Sara Kalvala
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 firstname.lastname@example.org