diff -r f89ee40fbb08 -r 78d828f43cdf Attic/FIXME-TODO
--- a/Attic/FIXME-TODO	Sat Dec 17 16:57:25 2011 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +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.
-
-- Provide syntax for different names of Abs and Rep functions
-  in a similar way to typedef
-
-    typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
-      morphisms list_of_dlist Abs_dlist
-
-- Allow defining constants with existing names.
-    Since 'insert' is defined for sets,
-    "quotient_definition insert" fails for fset
-    however "definition" succeeds.
-
-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, Dlist.
-
-- The current syntax of the quotient_definition is
-
-      "qconst :: qty"
-      as "rconst"
-
-  Is it possible to have the more Isabelle-like
-  syntax
-   
-      qconst :: "qty"
-      as "rconst"
-
-  That means "qconst :: qty" is not read as a term, but
-  as two entities.