aboutsummaryrefslogtreecommitdiff
path: root/isar
diff options
context:
space:
mode:
authorDavid Aspinall2004-04-16 17:46:24 +0000
committerDavid Aspinall2004-04-16 17:46:24 +0000
commit90ea182ba3992b16101d62725449f36d66e62bbd (patch)
tree7e4062d639e7ce936cc00f7b7e465e82e39050a9 /isar
parentff17818207cd996554e8eb17890388493ed63257 (diff)
Updated.
Diffstat (limited to 'isar')
-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