FIXME-TODO
changeset 503 d2c9a72e52e0
child 506 91c374abde06
child 512 8c7597b19f0e
--- /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 \<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
+
+- 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