diff -r 3d7a9d4d2bb6 -r 1e08743b6997 FIXME-TODO --- 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