Re: [isabelle] defining nat1 in isabelle



Hi Stephan,

Am 16.04.2013 um 15:02 schrieb Stephan van Staden <Stephan.vanStaden at inf.ethz.ch>:

> I think this use of "typedef" is deprecated. Although Isabelle still accepts it, I remember seeing warnings.

"Typedef" is still as encouraged as ever (modulo Tobias's warnings about the lack of automation). The warnings were probably tied to a specific usage of typedef. This is from the "NEWS" file:

    * Simplified 'typedef' specifications: historical options for implicit
    set definition and alternative name have been discontinued.  The
    former behavior of "typedef (open) t = A" is now the default, but
    written just "typedef t = A".  INCOMPATIBILITY, need to adapt theories
    accordingly.

If I recall right, during the transition period, "typedef" without "open" used to generate a warning.

Regards,

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.