diff -r db158e995bfc -r 9df6144e281b FIXME-TODO
--- a/FIXME-TODO	Thu Feb 25 07:48:57 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-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
-