diff -r ab942ba2d243 -r c093b2e6e9ae FIXME-TODO
--- a/FIXME-TODO	Sun Feb 21 22:39:11 2010 +0100
+++ b/FIXME-TODO	Mon Feb 22 09:55:43 2010 +0100
@@ -8,9 +8,6 @@
 Higher Priority
 ===============
 
-- Ask Markus how the files Quot* should be named.
-  (There is a HOL/Library/Quotient.thy --- seems to be an example. *)
-
 - If the constant definition gives the wrong definition
   term, one gets a cryptic message about absrep_fun
 
@@ -21,7 +18,6 @@
 - The user should be able to give quotient_respects and 
   preserves theorems in a more natural form.
 
-
 Lower Priority
 ==============
 
@@ -60,3 +56,6 @@
 
   That means "qconst :: qty" is not read as a term, but
   as two entities.
+
+- Restrict automatic translation to particular quotient types
+