Added Brian's suggestion.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 22 Feb 2010 10:16:13 +0100
changeset 1204 7e9e96158025
parent 1203 c093b2e6e9ae
child 1205 acbf50e8eac2
Added Brian's suggestion.
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