Re: [isabelle] Declaring equal for a type; BNF not working on the left



Hi Gottfried,

> I don't care that I can't make fun work with datatype_new, as long as primrec_new is working for me.

Once the next release is out, one of our first priorities will be to make sure "fun", the code generator, Quickcheck, Nitpick, etc., work with "datatype_new" just like they do with "datatype". We're currently waiting to avoid too much divergence between the release branch (from which the release candidates are generated) and the development branch (which will lead to the next-to-next Isabelle release).

Regards,

Jasmin





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