aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2000-08-03 16:53:41 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2000-08-03 16:53:41 +0000
commit89b4dc8fa2acb4f6ab93e9501db044071e196c6f (patch)
treed7aeea45bf62f99909ac70f1e737a702807085b4 /isar
parentf314918abd4430d0f8e1e0b6f7c6446a9f4510bc (diff)
** B make help key bindings appear in "Show me ..." menu;
Diffstat (limited to 'isar')
-rw-r--r--isar/todo4
1 files changed, 3 insertions, 1 deletions
diff --git a/isar/todo b/isar/todo
index f0be8852..5bb5500e 100644
--- a/isar/todo
+++ b/isar/todo
@@ -4,6 +4,8 @@
See also ../todo for generic things to do, priority codes.
+** B make help key bindings appear in "Show me ..." menu;
+
** C undo 'use' command: unlock corresponding ML file;
** C provide template for empty theory (or even just for Scratch.thy);
@@ -20,4 +22,4 @@ 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).
-
+ \ No newline at end of file