TODO
changeset 15412 7f373e478a5a
parent 15391 797ed46d724b
child 15414 d945f05e75a2
equal deleted inserted replaced
15411:1d195de59497 15412:7f373e478a5a
    10   as a setting (Stefan & Tjark)
    10   as a setting (Stefan & Tjark)
    11 
    11 
    12 - check/establish conformity of HTML files to (some version of) the HTML
    12 - check/establish conformity of HTML files to (some version of) the HTML
    13   language specification (cf. http://validator.w3.org/) (Tjark, or anyone
    13   language specification (cf. http://validator.w3.org/) (Tjark, or anyone
    14   who is interested)
    14   who is interested)
    15 
    15   
    16 - eliminate the last remaining old-style theories (Larry):  
    16 - 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.
    17   HOL_lemmas.ML
       
    18   NatArith.ML
       
    19   Relation_Power.ML
       
    20   
    17   
    21 - update or remove ex/MT (Larry? Tobias?)  
    18 - update or remove ex/MT (Larry? Tobias?)  
    22 
    19 
       
    20 - Include IsaPlanner? (Larry to co-ordinate)
       
    21 
    23 - remove this file (Tobias)
    22 - remove this file (Tobias)