--- 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
+