# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1324371514 -32400
# Node ID 16b5f41890758419ca4f5b00ece8103e0ec19cb8
# Parent  a6b0220fb8aeed073675792d76a91f4aac3bb211
Update Quotient FIXME-TODO, some issues were already fixed.

diff -r a6b0220fb8ae -r 16b5f4189075 Attic/FIXME-TODO
--- a/Attic/FIXME-TODO	Tue Dec 20 17:54:53 2011 +0900
+++ b/Attic/FIXME-TODO	Tue Dec 20 17:58:34 2011 +0900
@@ -18,17 +18,6 @@
 - 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
 ==============
 
@@ -53,18 +42,4 @@
   [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.
+- Examples: Finite multiset.