diff -r db158e995bfc -r 9df6144e281b Attic/FIXME-TODO
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/FIXME-TODO	Thu Feb 25 07:57:17 2010 +0100
@@ -0,0 +1,69 @@
+Highest Priority
+================
+
+- give examples for the new quantifier translations in regularization
+  (quotient_term.ML)
+
+
+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
+
+- Handle theorems that include Ball/Bex. For this, would 
+  it help if we introduced separate Bex and Ball constants 
+  for quotienting?
+
+- The user should be able to give quotient_respects and 
+  preserves theorems in a more natural form.
+
+Lower Priority
+==============
+
+- accept partial equivalence relations
+
+- think about what happens if things go wrong (like
+  theorem cannot be lifted) / proper diagnostic 
+  messages for the user
+
+- inductions from the datatype package have a strange
+  order of quantifiers in assumptions.
+
+- find clean ways how to write down the "mathematical"
+  procedure for a possible submission (Peter submitted 
+  his work only to TPHOLs 2005...we would have to go
+  maybe for the Journal of Formalised Mathematics)
+
+- add tests for adding theorems to the various thm lists
+
+- Maybe quotient and equiv theorems like the ones for
+  [QuotList, QuotOption, QuotPair...] could be automatically
+  proven?
+
+- Examples: Finite multiset.
+
+- The current syntax of the quotient_definition is
+
+      "qconst :: qty"
+      as "rconst"
+
+  Is it possible to have the more Isabelle-like
+  syntax
+   
+      qconst :: "qty"
+      as "rconst"
+
+  That means "qconst :: qty" is not read as a term, but
+  as two entities.
+
+- Restrict automatic translation to particular quotient types
+