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

- better lookup mechanism for quotient definition
  (see fixme in quotient_term.ML)

- check needs to be fixed in mk_resp_arg (quotient_term.ML),
  see test for (_, Const _)

- clever code in quotiet_tacs.ML needs to be turned into
  boring code

- comment about regularize tactic eeds to be adapted

- Check all the places where we do "handle _"
  (They make code changes very difficult: I sat 1/2
  a day over simplification of calculate_inst before
  I understood things; the reason was that my exceptions
  where caught by the catch all. There is no problem
  with throwing and handling exceptions...it just must
  be clear who throws what ad what is thrown.)

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

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

- have FSet.thy to have a simple infrastructure for 
  finite sets (syntax should be \<lbrace> \<rbrace>,
  look at Set.thy how syntax is been introduced)

- Handle theorems that include Ball/Bex. Would it help 
  if we introduced separate Bex and Ball constants for 
  quotienting?

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



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

- Maybe a quotient_definition should already require
  a proof of the respectfulness (in this way one
  already excludes non-sensical definitions)

- 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 that translates an an original theorem given
  a list of quotient_types 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)

- use lower-case letters where appropriate in order
  to make Markus happy

- add tests for adding theorems to the various thm lists

- We shouldn't use the command 'quotient' as this shadows Larry's quotient.
  Call it 'quotient_type'

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