18 

    18 

    19 

    19 

    20 Lower Priority

    20 Lower Priority

    21 ==============

    21 ==============

    22 

    22 

    23 - inductions from the datatype package have a strange

    25 - inductions from the datatype package have a strange

    24   order of quantifiers in assumptions.

    26   order of quantifiers in assumptions.

    25 

    27 

    26 - wrapper that translates an an original theorem given

    28 - wrapper that translates an an original theorem given

    27   a list of quotient_types as an attribute

    29   a list of quotient_types as an attribute

    31 

    30 

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

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

    33   procedure for a possible submission (Peter submitted 

    32   procedure for a possible submission (Peter submitted 

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

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

    35   maybe for the Journal of Formalised Mathematics)

    34   maybe for the Journal of Formalised Mathematics)