diff options
author | Makarius Wenzel <makarius@sketis.net> | 2006-12-30 14:49:59 +0000 |
---|---|---|
committer | Makarius Wenzel <makarius@sketis.net> | 2006-12-30 14:49:59 +0000 |
commit | b04ef68c5298cbcc1e22eb40e9595a60ae69d017 (patch) | |
tree | 902d3bec3602f471e4ccff59c7496a7736eae01a /isar | |
parent | 57db4d603f3ea66794278a39fa7eacdc6aed9b02 (diff) |
tuned;
Diffstat (limited to 'isar')
-rw-r--r-- | isar/todo | 9 |
1 files changed, 1 insertions, 8 deletions
@@ -24,12 +24,6 @@ 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 - Isar interface would allow (unless we send an ML file - line-by-line with ML_command?) - ** B theorem dependencies: using Isar's "thm" command does not work at top level. This is annoying for browsing the fully qualified dependency names. (Even the ML_command "thm" @@ -52,5 +46,4 @@ See also ../todo for generic things to do, priority codes. ** C provide template for empty theory (or even just for Scratch.thy); -** C proper proof-by-pointing support (hard; needs major reworking of - Isabelle's pretty-printing subsystem); +** C proper proof-by-pointing support (vary hard); |