--- a/Attic/FIXME-TODO	Sun Jun 19 13:14:37 2011 +0900
+++ b/Attic/FIXME-TODO	Mon Jun 20 08:50:13 2011 +0900
@@ -8,22 +8,14 @@
 Higher Priority
 ===============
 
-
-- Also, in the interest of making nicer generated documentation, you
-  might want to change all your "section" headings in Quotient.thy to
-  "subsection", and add a "header" statement to the top of the file.
-  Otherwise, each "section" gets its own chapter in the generated pdf,
-  when the rest of HOL has one chapter per theory file (the chapter
-  title comes from the "header" statement).
-
 - If the constant definition gives the wrong definition
   term, one gets a cryptic message about absrep_fun
 
-- Handle theorems that include Ball/Bex. For this, would 
-  it help if we introduced separate Bex and Ball constants 
-  for quotienting?
+- 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 
+- The user should be able to give quotient_respects and
   preserves theorems in a more natural form.
 
 Lower Priority
@@ -32,8 +24,6 @@
 - the quot_lifted attribute should rename variables so they do not
   suggest that they talk about raw terms.
 
-- accept partial equivalence relations
-
 - think about what happens if things go wrong (like
   theorem cannot be lifted) / proper diagnostic 
   messages for the user
@@ -52,7 +42,7 @@
   [QuotList, QuotOption, QuotPair...] could be automatically
   proven?
 
-- Examples: Finite multiset.
+- Examples: Finite multiset, Dlist.
 
 - The current syntax of the quotient_definition is