From b04ef68c5298cbcc1e22eb40e9595a60ae69d017 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Sat, 30 Dec 2006 14:49:59 +0000
Subject: tuned;

---
 isar/todo | 9 +--------
 1 file changed, 1 insertion(+), 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);
-- 
cgit v1.2.3