Highest Priority================- give examples for the new quantifier translations in regularization (quotient_term.ML)Higher Priority===============- If the constant definition gives the wrong definition term, one gets a cryptic message about absrep_fun- Handle theorems that include Ball/Bex. Workaround: Unfolding Ball_def/Bex_def is enough to lift, in some cases regularization is harder though.- The user should be able to give quotient_respects and preserves theorems in a more natural form.Lower Priority==============- the quot_lifted attribute should rename variables so they do not suggest that they talk about raw terms.- 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.- 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)- add tests for adding theorems to the various thm lists- Maybe quotient and equiv theorems like the ones for [QuotList, QuotOption, QuotPair...] could be automatically proven?- Examples: Finite multiset.