Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations.
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 - Handle theorems that include Ball/BexLower 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.