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)+
−