aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall2004-04-16 17:46:24 +0000
committerDavid Aspinall2004-04-16 17:46:24 +0000
commit90ea182ba3992b16101d62725449f36d66e62bbd (patch)
tree7e4062d639e7ce936cc00f7b7e465e82e39050a9
parentff17818207cd996554e8eb17890388493ed63257 (diff)
Updated.
-rw-r--r--isar/todo2
1 files changed, 2 insertions, 0 deletions
diff --git a/isar/todo b/isar/todo
index e6d3ed1d..3740ade2 100644
--- a/isar/todo
+++ b/isar/todo
@@ -4,6 +4,8 @@
See also ../todo for generic things to do, priority codes.
+** C Electric terminator for non-terminator provers would be nice.
+
** B Isabelle support for ML and legacy files: would like to remove "isa" instance
Could we handle theory files and even allow scripting in ML files
at the same time as Isar? Maybe not, if this is even beyond what