Isabelle Proof General Written by David Aspinall, later with assistance from Markus Wenzel and David von Oheimb. $Id$ Status: supported Maintainer: David Aspinall Isabelle version: 99 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 proper 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. There is no support for proof by pointing yet, and no tags program. 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.