Highest Priority================- give examples for the new quantifier translations in regularization (quotient_term.ML)Higher Priority===============- Also, in the interest of making nicer generated documentation, you might want to change all your "section" headings in Quotient.thy to "subsection", and add a "header" statement to the top of the file. Otherwise, each "section" gets its own chapter in the generated pdf, when the rest of HOL has one chapter per theory file (the chapter title comes from the "header" statement).- 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==============- the quot_lifted attribute should rename variables so they do not suggest that they talk about raw terms.- 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.- 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.