Highest Priority================- give examples for the new quantifier translations in regularization (quotient_term.ML)Higher Priority===============- Ask Markus how the files Quot* should be named. (There is a HOL/Library/Quotient.thy --- seems to be an example. *)- Is Bexeq the right name?- If the constant definition gives the wrong definition term, one gets a cryptic message about absrep_fun- Handle theorems that include Ball/Bex. For this, would it help if we introduced separate Bex and Ball constants for quotienting?- The user should be able to give quotient_respects and preserves theorems in a more natural form.Lower Priority==============- accept partial equivalence relations- 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.- wrapper for lifting ... to be used 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)- 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.- The current syntax of the quotient_definition is "qconst :: qty" as "rconst" Is it possible to have the more Isabelle-like syntax qconst :: "qty" as "rconst" That means "qconst :: qty" is not read as a term, but as two entities.- Add syntax for Bexeq, for example "\<exists>!!"