aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2000-09-13 20:41:11 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2000-09-13 20:41:11 +0000
commitfaea801b0156d4ab9b1c133eb509a5ba377afef1 (patch)
tree43d64ba0ad1028fb1225dd0b4567a3e27e4c16ef
parent16abe31496ad0baa426c8941fcc49b3285009940 (diff)
done: make help key bindings appear in "Show me ..." menu;
-rw-r--r--isar/todo2
1 files changed, 0 insertions, 2 deletions
diff --git a/isar/todo b/isar/todo
index 5bb5500e..3ad7f7c2 100644
--- a/isar/todo
+++ b/isar/todo
@@ -4,8 +4,6 @@
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);