--- a/FIXME-TODO	Thu Dec 03 14:02:05 2009 +0100
+++ b/FIXME-TODO	Thu Dec 03 15:03:31 2009 +0100
@@ -24,7 +24,15 @@
 Lower Priority
 ==============
 
+- allow the user to provide the rsp lemmas in a more
+  natural form
+
 - find clean ways how to write down the "mathematical"
   procedure for a possible submission (Peter submitted 
   his work only to TPHOLs 2005...we would have to go
-  maybe for the Journal of Formalised Mathematics)
\ No newline at end of file
+  maybe for the Journal of Formalised Mathematics)
+
+- use lower-case letters where appropriate in order
+  to make Markus happy
+
+- add tests for adding theorems to the various thm lists
\ No newline at end of file