diff -r 6b2f6e7e62cc -r d2c9a72e52e0 FIXME-TODO --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/FIXME-TODO Thu Dec 03 13:59:53 2009 +0100 @@ -0,0 +1,30 @@ +Higher Priority +=============== + +- redoing Int.thy (problem at the moment with overloaded + definitions....Florian) + +- have FSet.thy to have a simple infrastructure for + finite sets (syntax should be \ \, + 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 + +- Ask Peter and Michael for challenging examples + + + + + + + + +Lower Priority +============== + +- 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 + maybe for the Journal of Formalised Mathematics) \ No newline at end of file