FIXME-TODO
changeset 514 6b3be083229c
parent 512 8c7597b19f0e
parent 506 91c374abde06
child 515 b00a9b58264d
equal deleted inserted replaced
513:eed5d55ea9a6 514:6b3be083229c
    25 
    25 
    26 
    26 
    27 Lower Priority
    27 Lower Priority
    28 ==============
    28 ==============
    29 
    29 
       
    30 - allow the user to provide the rsp lemmas in a more
       
    31   natural form
       
    32 
    30 - find clean ways how to write down the "mathematical"
    33 - find clean ways how to write down the "mathematical"
    31   procedure for a possible submission (Peter submitted 
    34   procedure for a possible submission (Peter submitted 
    32   his work only to TPHOLs 2005...we would have to go
    35   his work only to TPHOLs 2005...we would have to go
    33   maybe for the Journal of Formalised Mathematics)
    36   maybe for the Journal of Formalised Mathematics)
       
    37 
       
    38 - use lower-case letters where appropriate in order
       
    39   to make Markus happy
       
    40 
       
    41 - add tests for adding theorems to the various thm lists