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- quotient_respects and preserves in a natural form.Lower Priority==============- accept partial equvalence relations- 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'