# HG changeset patch
# User paulson
# Date 1103102359 -3600
# Node ID 7f373e478a5ad216840678d81a532f03434c9df7
# Parent  1d195de594970784c8789003bcdedd90bf98f909
*** empty log message ***

diff -r 1d195de59497 -r 7f373e478a5a TODO
--- a/TODO	Wed Dec 15 10:19:01 2004 +0100
+++ b/TODO	Wed Dec 15 10:19:19 2004 +0100
@@ -12,12 +12,11 @@
 - 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)
-
-- eliminate the last remaining old-style theories (Larry):  
-  HOL_lemmas.ML
-  NatArith.ML
-  Relation_Power.ML
+  
+- fix the inductive definition bug (Larry): Equations in the intro rules can make proofs fail. Perhaps the critical proof could "protect" the initial equations e.g. by disjoining False, and removing this later.
   
 - update or remove ex/MT (Larry? Tobias?)  
 
+- Include IsaPlanner? (Larry to co-ordinate)
+
 - remove this file (Tobias)