[isabelle-dev] docs for new datatype package

Gerwin Klein Gerwin.Klein at nicta.com.au
Sun Apr 19 16:45:31 CEST 2015


The datatype manual says in e8472fc02fe5:

"The datatype_compat command is needed to register new-style datatypes for use with fun and function (Section 2.2.2)"

Is this still correct?

Cheers,
Gerwin

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


More information about the isabelle-dev mailing list