diff -r 139b257e10d2 -r 551eacf071d7 FIXME-TODO
--- a/FIXME-TODO	Tue Feb 09 14:32:37 2010 +0100
+++ b/FIXME-TODO	Tue Feb 09 15:28:15 2010 +0100
@@ -11,9 +11,6 @@
 - Ask Markus how the files Quot* should be named.
   (There is a HOL/Library/Quotient.thy --- seems to be an example. *)
 
-- Is Bexeq the right name?
-
-
 - If the constant definition gives the wrong definition
   term, one gets a cryptic message about absrep_fun
 
@@ -37,8 +34,6 @@
 - inductions from the datatype package have a strange
   order of quantifiers in assumptions.
 
-- wrapper for lifting ... to be used as an attribute
-
 - 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
@@ -65,5 +60,3 @@
 
   That means "qconst :: qty" is not read as a term, but
   as two entities.
-
-- Add syntax for Bexeq, for example "\<exists>!!"