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.- Provide syntax for different names of Abs and Rep functions in a similar way to typedef typedef (open) 'a dlist = "{xs::'a list. distinct xs}" morphisms list_of_dlist Abs_dlist- Allow defining constants with existing names. Since 'insert' is defined for sets, "quotient_definition insert" fails for fset however "definition" succeeds.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, Dlist.- 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.