aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2001-08-30 19:41:27 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2001-08-30 19:41:27 +0000
commitd2a785370e33b82d31e23b4564aa1785d231a437 (patch)
tree73363f50ade0f945e6ccce0a0d2fdf127a824d2d
parentda0a521b5a69220eca07794daec9c55cfad9ec2a (diff)
updated;
-rw-r--r--isa/README3
-rw-r--r--isar/README2
-rw-r--r--isar/todo3
3 files changed, 2 insertions, 6 deletions
diff --git a/isa/README b/isa/README
index ef43f82a..b59e4671 100644
--- a/isa/README
+++ b/isa/README
@@ -7,7 +7,7 @@ $Id$
Status: supported
Maintainer: David Aspinall
-Isabelle version: 99-1
+Isabelle version: 99-1, 99-2
Isabelle homepage: http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
========================================
@@ -26,4 +26,3 @@ 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.
-
diff --git a/isar/README b/isar/README
index c87965ce..671d0920 100644
--- a/isar/README
+++ b/isar/README
@@ -6,7 +6,7 @@ $Id$
Status: supported
Maintainer: Markus Wenzel
-Isabelle version: 99-1
+Isabelle version: 99-1, 99-2
Isabelle homepage: http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
Isar homepage: http://isabelle.in.tum.de/Isar/
diff --git a/isar/todo b/isar/todo
index 912019c0..0266533d 100644
--- a/isar/todo
+++ b/isar/todo
@@ -17,9 +17,6 @@ Isabelle's pretty-printing subsystem);
** C tune behaviour of goals/response buffers (e.g. hide empty
response buffers when using 2 buffer model);
-** D Combine with isa/ to get single Isabelle PG instance, somehow?
-Then users could use both proof languages in the same session.
-
** D Fixup so that typing in shell buffer updates locked buffer status.
It works in Isabelle/classic, why not here? (But users shouldn't
type in shell buffer, anyway).