Highest Priority
================

- give examples for the new quantifier translations in regularization
  (quotient_term.ML)


Higher Priority
===============

- If the constant definition gives the wrong definition
  term, one gets a cryptic message about absrep_fun

- Handle theorems that include Ball/Bex.
  Workaround: Unfolding Ball_def/Bex_def is enough to lift,
    in some cases regularization is harder though.

- The user should be able to give quotient_respects and
  preserves theorems in a more natural form.

- Provide syntax for different names of Abs and Rep functions
  in a similar way to typedef

    typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
      morphisms list_of_dlist Abs_dlist

- Allow defining constants with existing names.
    Since 'insert' is defined for sets,
    "quotient_definition insert" fails for fset
    however "definition" succeeds.

Lower Priority
==============

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

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

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