TODO
changeset 15412 7f373e478a5a
parent 15391 797ed46d724b
child 15414 d945f05e75a2
--- 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)