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

- redoing Int.thy (problem at the moment with overloaded
  definitions....Florian)

- 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

- Ask Peter and Michael for challenging examples
  And for examples where it is useful to lift types
  over a relation being only a partial equivalence



- Handle theorems that include Ball/Bex

- Test theorems with abstractions





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

- allow the user to provide the rsp lemmas in a more
  natural form

- 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



- Integrate RSP/PRS lemmas in QuotList with the ones from IntEx etc.

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