1 Higher Priority

     2 ===============

     3 

     4 - redoing Int.thy (problem at the moment with overloaded

     5   definitions....Florian)

     6 

     7 - have FSet.thy to have a simple infrastructure for 

     8   finite sets (syntax should be \<lbrace> \<rbrace>,

     9   look at Set.thy how syntax is been introduced)

    10 

    11 - think about what happens if things go wrong (like

    12   theorem cannot be lifted) / proper diagnostic 

    13   messages for the user

    14 

    15 - Ask Peter and Michael for challenging examples 

    16 

    17 

    18 

    19 

    20 

    21 

    22 

    23 

    24 Lower Priority

    25 ==============

    26 

    27 - find clean ways how to write down the "mathematical"

    28   procedure for a possible submission (Peter submitted 

    29   his work only to TPHOLs 2005...we would have to go

    30   maybe for the Journal of Formalised Mathematics)