diff -r c093b2e6e9ae -r 7e9e96158025 FIXME-TODO
--- a/FIXME-TODO	Mon Feb 22 09:55:43 2010 +0100
+++ b/FIXME-TODO	Mon Feb 22 10:16:13 2010 +0100
@@ -8,6 +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