diff -r 37285ec4387d -r e9e205b904e2 FIXME-TODO
--- a/FIXME-TODO	Sun Dec 20 00:53:35 2009 +0100
+++ b/FIXME-TODO	Mon Dec 21 22:36:31 2009 +0100
@@ -8,11 +8,9 @@
   finite sets (syntax should be \<lbrace> \<rbrace>,
   look at Set.thy how syntax is been introduced)
 
-- think about what happens if things go wrong (like
-  theorem cannot be lifted) / proper diagnostic 
-  messages for the user
-
-- Handle theorems that include Ball/Bex
+- Handle theorems that include Ball/Bex. Would it help 
+  if we introduced separate Bex and Ball constants for 
+  quotienting?
 
 - user should be able to give quotient_respects and 
   preserves theorems in a more natural form.
@@ -22,12 +20,15 @@
 Lower Priority
 ==============
 
+- Maybe a quotient_definition should already require
+  a proof of the respectfulness (in this way one
+  already excludes non-sensical definitions)
+
 - accept partial equvalence relations
 
-- what happens if the original theorem contains bounded
-  quantifiers? can such theorems be lifted? If not, would 
-  it help if we introduced separate Bex and Ball constants
-  for quotienting?
+- 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.
@@ -55,4 +56,18 @@
   [QuotList, QuotOption, QuotPair...] could be automatically
   proven?
 
-- Examples: Finite multiset.
\ No newline at end of file
+- 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.
\ No newline at end of file