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.+
−