*** empty log message ***
authorpaulson
Fri, 17 Dec 2004 10:15:10 +0100
changeset 15417 b488b290eccb
parent 15416 db69af736ebb
child 15418 e28853da5df5
*** empty log message ***
TODO
--- a/TODO	Thu Dec 16 14:34:23 2004 +0100
+++ b/TODO	Fri Dec 17 10:15:10 2004 +0100
@@ -13,8 +13,6 @@
   language specification (cf. http://validator.w3.org/) (Tjark, or anyone
   who is interested)
   
-- 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)