# HG changeset patch
# User nipkow
# Date 1103563522 -3600
# Node ID 7a91490c1b04db1bcf50b0a6fe3af9311e2776bd
# Parent  761a4f8e6ad6f084d890a8c35f16929e72a79c34
*** empty log message ***

diff -r 761a4f8e6ad6 -r 7a91490c1b04 TODO
--- a/TODO	Sat Dec 18 17:14:33 2004 +0100
+++ b/TODO	Mon Dec 20 18:25:22 2004 +0100
@@ -4,7 +4,9 @@
 
 - modular generation of ML code with structures (Stefan)
 
-- finding rewrite rules based on PG subterm selection (Tobias)
+> Unfortunately when ?s are switched off during building Isabelle this 
+> broke something inside the datatype package (for Isar I think)
+  (Stefan)
 
 - a global "disprove" menu item both as an action and (if it can be done)
   as a setting (Stefan & Tjark)
@@ -13,7 +15,7 @@
   language specification (cf. http://validator.w3.org/) (Tjark, or anyone
   who is interested)
   
-- update or remove ex/MT (Larry? Tobias?)  
+- update or remove ex/MT (Larry)  
 
 - Include IsaPlanner? (Larry to co-ordinate)