Updated.

2 files changed, 19 insertions, 4 deletions

diff --git a/coq/todo b/coq/todo
index 607c6729..4515e9c4 100644
--- a/coq/todo
+++ b/coq/todo
@@ -5,7 +5,16 @@
 See also ../todo for generic things to do, priority codes.
 
 
-** B Proof-by-Pointing [1 month]
+** C Auto-compile-vos
+   Would be nice to ressurect this: interaction between PG
+   and make system is tricky and tedious.  
+
+
+** D Loss of synchronisation with silent mode 
+   Apocryphal story, no test cases.
+
+
+** B Proof-by-Pointing [1 month+]  (2002)
   da: Yves Bertot told me that his CtCoq proof-by-pointing code
   is in the Coq kernel now, so would be useful for PG.
   We need a Coq hacker to do this.
diff --git a/isar/todo b/isar/todo
index 0adc6508..e6d3ed1d 100644
--- a/isar/todo
+++ b/isar/todo
@@ -4,6 +4,12 @@
 
 See also ../todo for generic things to do, priority codes.
 
+** 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"
@@ -12,12 +18,12 @@ See also ../todo for generic things to do, priority codes.
 
 ** B visualise dependencies: sometimes not applicable.
 
-** C func-menu: observe proof-syntactic-context (general problem of
-func-menu setup?);
+** C func-menu: 
+	observe proof-syntactic-context (general problem of func-menu setup?);
 
 ** C undo 'use' command: unlock corresponding ML file;
 
 ** 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);
+     Isabelle's pretty-printing subsystem);