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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
