1 Highest Priority

     2 ================

     3 

     4 - give examples for the new quantifier translations in regularization

     5   (quotient_term.ML)

     6 

     7 

     8 Higher Priority

     9 ===============

    10 

    11 - If the constant definition gives the wrong definition

    12   term, one gets a cryptic message about absrep_fun

    13 

    14 - Handle theorems that include Ball/Bex.

    15   Workaround: Unfolding Ball_def/Bex_def is enough to lift,

    16     in some cases regularization is harder though.

    17 

    18 - The user should be able to give quotient_respects and

    19   preserves theorems in a more natural form.

    20 

    21 Lower Priority

    22 ==============

    23 

    24 - the quot_lifted attribute should rename variables so they do not

    25   suggest that they talk about raw terms.

    26 

    27 - think about what happens if things go wrong (like

    28   theorem cannot be lifted) / proper diagnostic 

    29   messages for the user

    30 

    31 - inductions from the datatype package have a strange

    32   order of quantifiers in assumptions.

    33 

    34 - find clean ways how to write down the "mathematical"

    35   procedure for a possible submission (Peter submitted 

    36   his work only to TPHOLs 2005...we would have to go

    37   maybe for the Journal of Formalised Mathematics)

    38 

    39 - add tests for adding theorems to the various thm lists

    40 

    41 - Maybe quotient and equiv theorems like the ones for

    42   [QuotList, QuotOption, QuotPair...] could be automatically

    43   proven?

    44 

    45 - Examples: Finite multiset.