--- a/FIXME-TODO	Tue Feb 23 13:32:35 2010 +0100
+++ b/FIXME-TODO	Tue Feb 23 13:33:01 2010 +0100
@@ -8,8 +8,13 @@
 Higher Priority
 ===============
 
-- Ask Markus how the files Quot* should be named.
-  (There is a HOL/Library/Quotient.thy --- seems to be an example. *)
+
+- 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
@@ -21,7 +26,6 @@
 - The user should be able to give quotient_respects and 
   preserves theorems in a more natural form.
 
-
 Lower Priority
 ==============
 
@@ -60,3 +64,6 @@
 
   That means "qconst :: qty" is not read as a term, but
   as two entities.
+
+- Restrict automatic translation to particular quotient types
+