(* -*- isa -*-
Example theory file for Isabelle
David Aspinall <da@dcs.ed.ac.uk>
$Id$
The line at the top of this comment forces
Proof General's classic Isabelle mode;
scripting takes place in .ML files.
NB: this is incompatible with PG/Isar.
*)
Example = Main