--- a/FIXME-TODO	Fri Dec 11 15:58:15 2009 +0100
+++ b/FIXME-TODO	Fri Dec 11 16:32:40 2009 +0100
@@ -20,15 +20,14 @@
 Lower Priority
 ==============
 
+- accept partial equvalence relations
+
 - 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 
   his work only to TPHOLs 2005...we would have to go