Updated

1 files 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.