# HG changeset patch
# User nipkow
# Date 1105980303 -3600
# Node ID 42b858b978b833bd17fd1e95daefbe5b835469dc
# Parent  d0cd75f7a3656a9b9dc8565e567886d9499c8838
*** empty log message ***

diff -r d0cd75f7a365 -r 42b858b978b8 TODO
--- a/TODO	Mon Jan 17 15:21:40 2005 +0100
+++ b/TODO	Mon Jan 17 17:45:03 2005 +0100
@@ -2,6 +2,8 @@
 
 - update course material slides to new theory format (Tobias)
 
+- attach additional ML code to consts_code section (Stefan)
+
 - modular generation of ML code with structures (Stefan)
 
 > Unfortunately when ?s are switched off during building Isabelle this 
@@ -14,11 +16,13 @@
 - check/establish conformity of HTML files to (some version of) the HTML
   language specification (cf. http://validator.w3.org/) (Tjark, or anyone
   who is interested)
-  
+
 - update or remove ex/MT (Larry)  
 
 - Include IsaPlanner? (Larry to co-ordinate)
 
 - update LaTeXsugar, remove references to future Isabelle2005 etc. (Gerwin)
 
+- rules -> iprover (Stefan)
+
 - remove this file (Tobias)