diff options
| -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); |