diff options
Diffstat (limited to 'isa/README')
| -rw-r--r-- | isa/README | 17 |
1 files changed, 16 insertions, 1 deletions
@@ -5,10 +5,25 @@ 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 no support for proof by pointing yet. +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. |