# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1308685796 -32400
# Node ID 05a4745b0a9d86cb5fa3eb89fffba465c52e255e
# Parent  186ec672cc5157222a9d8053a9aa3d0280ad03f6
Quotients/TODO addtion

diff -r 186ec672cc51 -r 05a4745b0a9d Attic/FIXME-TODO
--- a/Attic/FIXME-TODO	Tue Jun 21 23:59:36 2011 +0900
+++ b/Attic/FIXME-TODO	Wed Jun 22 04:49:56 2011 +0900
@@ -18,6 +18,12 @@
 - 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
+
 Lower Priority
 ==============