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.