Isabelle Proof General Written by David Aspinall, later with assistance from Markus Wenzel and David von Oheimb. Status: supported Maintainer: David Aspinall Isabelle versions: Isabelle99-1, Isabelle99-2, Isabelle2002 Isabelle homepage: http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ ======================================== Isabelle Proof General has full support for multiple file scripting, with dependencies between theories communicated between Isabelle and Proof General. It has a mode for editing theory files taken from Isamode. There is excellent support for X Symbol, using the Isabelle print mode for X Symbol tokens. Many Isabelle theories have X Symbol syntax already defined and it's easy to add to your own theories. The script `interface' and file 'interface-setup.el' are used to start Isabelle Proof General via the 'Isabelle' shell command. These files were provided by Markus Wenzel. Check the value of isabelle-prog-name. ======================================== $Id$