aboutsummaryrefslogtreecommitdiff
path: root/isa/README
diff options
context:
space:
mode:
Diffstat (limited to 'isa/README')
-rw-r--r--isa/README31
1 files changed, 31 insertions, 0 deletions
diff --git a/isa/README b/isa/README
new file mode 100644
index 00000000..b99be777
--- /dev/null
+++ b/isa/README
@@ -0,0 +1,31 @@
+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$
+