--- a/FIXME-TODO	Fri Dec 11 11:32:29 2009 +0100
+++ b/FIXME-TODO	Fri Dec 11 13:51:08 2009 +0100
@@ -1,8 +1,6 @@
 Higher Priority
 ===============
 
-- handling constant definitions is ugly at the moment
-
 - if the constant definition gives the wrong definition
   term, one gets a cryptic message about get_fun
 
@@ -14,23 +12,22 @@
   theorem cannot be lifted) / proper diagnostic 
   messages for the user
 
-- Ask Peter and Michael for challenging examples
-  And for examples where it is useful to lift types
-  over a relation being only a partial equivalence
-
 - Handle theorems that include Ball/Bex
 
-- Test theorems with abstractions
-
-
-
+- quotient_respects and preserves in a natural form.
 
 
 Lower Priority
 ==============
 
-- allow the user to provide the rsp lemmas in a more
-  natural form
+- inductions from the datatype package have a strange
+  order of quantifiers in assumptions.
+
+- wrapper that translates an an original theorem given
+  a list of quotient_types as an attribute
+
+
+
 
 - find clean ways how to write down the "mathematical"
   procedure for a possible submission (Peter submitted 
@@ -43,9 +40,6 @@
 - add tests for adding theorems to the various thm lists
 
 
-
-- Integrate RSP/PRS lemmas in QuotList with the ones from IntEx etc.
-
 - Check all the places where we do "handle _"
 
 - We shouldn't use the command 'quotient' as this shadows Larry's quotient.