Slides
Slides 1
Slides 2
Slides 3
Example Theories from the Lectures
Minimal.thy
Lec1.thy
Lec2.thy
CK_Machine.thy
CK_Machine_full.thy
Download and Installation
You need four packages: Polyml, Isabelle 2008, an emacs and Proof General:
Download
Installation Notes
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
details.
Once you have Isabelle running make sure XSymbols are switched on
and the HOL-Nominal heap is loaded.
More Examples
See src/HOL/Nominal/Examples in the place where you have installed Isabelle.