diff -r aa157e957655 -r 91b079db7380 FIXME-TODO --- a/FIXME-TODO Thu Dec 10 16:56:03 2009 +0100 +++ b/FIXME-TODO Thu Dec 10 18:28:30 2009 +0100 @@ -1,8 +1,10 @@ Higher Priority =============== -- redoing Int.thy (problem at the moment with overloaded - definitions....Florian) +- handling constant definitions is ugly at the moment + +- if the constant definition gives the wrong definition + term, one gets a cryptic message about get_fun - have FSet.thy to have a simple infrastructure for finite sets (syntax should be \ \, @@ -16,8 +18,6 @@ And for examples where it is useful to lift types over a relation being only a partial equivalence - - - Handle theorems that include Ball/Bex - Test theorems with abstractions