--- a/FIXME-TODO Thu Feb 25 07:48:57 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-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
-==============
-
-- 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.
-
-- Restrict automatic translation to particular quotient types
-