8 Higher Priority

     8 Higher Priority

     9 ===============

     9 ===============

    10 

    10 

    11 - Ask Markus how the files Quot* should be named.

    11 - Ask Markus how the files Quot* should be named.

    12   (There is a HOL/Library/Quotient.thy --- seems to be an example. *)

    12   (There is a HOL/Library/Quotient.thy --- seems to be an example. *)

    16 

    13 

    17 - If the constant definition gives the wrong definition

    14 - If the constant definition gives the wrong definition

    18   term, one gets a cryptic message about absrep_fun

    15   term, one gets a cryptic message about absrep_fun

    19 

    16 

    20 - Handle theorems that include Ball/Bex. For this, would 

    17 - Handle theorems that include Ball/Bex. For this, would 

    34   theorem cannot be lifted) / proper diagnostic 

    31   theorem cannot be lifted) / proper diagnostic 

    35   messages for the user

    32   messages for the user

    36 

    33 

    37 - inductions from the datatype package have a strange

    34 - inductions from the datatype package have a strange

    38   order of quantifiers in assumptions.

    35   order of quantifiers in assumptions.

    41 

    36 

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

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

    43   procedure for a possible submission (Peter submitted 

    38   procedure for a possible submission (Peter submitted 

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

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

    45   maybe for the Journal of Formalised Mathematics)

    40   maybe for the Journal of Formalised Mathematics)

    63       qconst :: "qty"

    58       qconst :: "qty"

    64       as "rconst"

    59       as "rconst"

    65 

    60 

    66   That means "qconst :: qty" is not read as a term, but

    61   That means "qconst :: qty" is not read as a term, but

    67   as two entities.

    62   as two entities.