--- a/FIXME-TODO	Fri Dec 04 09:08:51 2009 +0100
+++ b/FIXME-TODO	Fri Dec 04 09:25:27 2009 +0100
@@ -27,7 +27,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)
+
+- 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