tuned;

1 files changed, 1 insertions, 8 deletions

diff --git a/isar/todo b/isar/todo
index 3c20c6b0..75da5f95 100644
--- a/isar/todo
+++ b/isar/todo
@@ -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);