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