aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar/README
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2000-09-19 09:42:19 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2000-09-19 09:42:19 +0000
commit41113572f109f81db301aab9ed828cb60438c4c8 (patch)
tree5046b616151336302104152f7da44631666ae49b /isar/README
parent328e653f123a71b43062a4bbc81cc503f60a0487 (diff)
Isabelle version: 99-1;
tuned;
Diffstat (limited to 'isar/README')
-rw-r--r--isar/README9
1 files changed, 6 insertions, 3 deletions
diff --git a/isar/README b/isar/README
index f9d0e689..c87965ce 100644
--- a/isar/README
+++ b/isar/README
@@ -6,7 +6,8 @@ $Id$
Status: supported
Maintainer: Markus Wenzel
-Isabelle version: 99
+Isabelle version: 99-1
+Isabelle homepage: http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
Isar homepage: http://isabelle.in.tum.de/Isar/
========================================
@@ -21,5 +22,7 @@ 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.
+The script `interface' and file 'interface-setup.el' are used
+internally to start Isabelle Proof General via the 'Isabelle' shell
+command. This is the default way to invoke Proof General from the
+Isabelle perspective.