--- a/Attic/FIXME-TODO Sat Dec 17 16:57:25 2011 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-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.