From ada49d04eccf9f94831ad7498cac436ecfbffd40 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 12 May 2000 17:27:03 +0000
Subject: Updated

---
 todo | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/todo b/todo
index ce7db622..80bfdf75 100644
--- a/todo
+++ b/todo
@@ -52,14 +52,14 @@ C Problem with startup for Coq and HOL.  See BUGS.
 
 **** A Doc new bits: Isabelle settings mechanism, win32 support
 
-**** A Add a new keymap(s) for proof assistants.
-  Presently they naughtily bind C-c <letter> which are reserved for
-  users.  As a prelude to introducing more prover-specific commands,
-  we should change these.  New map choices:
-
-    C-c C-a (but blasts command start)
-    C-c C-p (blasts proof-prf)
-    C-c C-x already seems to be a prefix?
+**** B New keymap(s) for proof assistants.  Added on C-c C-a
+
+   Doc this change.
+   Means old C-c C-a and C-c C-e are lost.
+   Consider adding new submap for movement in proof script.
+
+**** C Isabelle: I think show_sorts -> show_types ?
+   
 
 **** A Add efficiency improvement by turning on/off prover output.
   Patch already added to pre-release.
-- 
cgit v1.2.3