Higher Priority

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

- if the constant definition gives the wrong definition

  term, one gets a cryptic message about get_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)

- think about what happens if things go wrong (like

  theorem cannot be lifted) / proper diagnostic 

  messages for the user

- Handle theorems that include Ball/Bex

- user should be able to give quotient_respects and 

  preserves theorems in a more natural form.

- the test in the (_, Const _) needs to be fixed

Lower Priority

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

- accept partial equvalence relations

- what happens if the original theorem contains bounded

  quantifiers? can such theorems be lifted? If not, would 

  it help if we introduced separate Bex and Ball constants

  for quotienting?

- 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

- Check all the places where we do "handle _"

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