--- a/Attic/FIXME-TODO	Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-Highest Priority
-================
-
-- give examples for the new quantifier translations in regularization
-  (quotient_term.ML)
-
-
-Higher Priority
-===============
-
-- If the constant definition gives the wrong definition
-  term, one gets a cryptic message about absrep_fun
-
-- Handle theorems that include Ball/Bex.
-  Workaround: Unfolding Ball_def/Bex_def is enough to lift,
-    in some cases regularization is harder though.
-
-- The user should be able to give quotient_respects and
-  preserves theorems in a more natural form.
-
-Lower Priority
-==============
-
-- the quot_lifted attribute should rename variables so they do not
-  suggest that they talk about raw terms.
-
-- think about what happens if things go wrong (like
-  theorem cannot be lifted) / proper diagnostic 
-  messages for the user
-
-- inductions from the datatype package have a strange
-  order of quantifiers in assumptions.
-
-- 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)
-
-- add tests for adding theorems to the various thm lists
-
-- Maybe quotient and equiv theorems like the ones for
-  [QuotList, QuotOption, QuotPair...] could be automatically
-  proven?
-
-- Examples: Finite multiset.