Highest Priority

================

- better lookup mechanism for quotient definition

  (see fixme in quotient_term.ML)

Higher Priority

===============

- If the user defines twice the same quotient constant,

  for example funion, then the line 

    val Free (lhs_str, lhs_ty) = lhs

  in quotient_def raises a bind exception.

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

- wrapper for lifting ... to be used as an attribute

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