Example Theories from the Lectures
Download and Installation
You need four packages: Polyml, Isabelle 2008, an emacs and Proof General:
Make sure you download the HOL-Nominal heap file. If you use MacOSX and not
already use Xemacs, then the easiest method to get Isabelle running is to
use Carbon Emacs and the latest version of ProofGeneral. Ask me for
Once you have Isabelle running make sure XSymbols are switched on
and the HOL-Nominal heap is loaded.
See src/HOL/Nominal/Examples in the place where you have installed Isabelle.