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

- the quot_lifted attribute should rename variables so they do not
  suggest that they talk about raw terms.

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