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