[isabelle-dev] docs for new datatype package

Gerwin Klein Gerwin.Klein at nicta.com.au
Tue Apr 21 21:40:00 CEST 2015

> On 21 Apr 2015, at 6:07 pm, Jasmin Blanchette <jasmin.blanchette at inria.fr> wrote:
> But when it comes to “size”, I’m sorry I didn’t make it more compatible with the old one. Thankfully, there’s an easy (if tedious) workaround.

Just found out that datatype_compat does declare the old size functions as they were before. They work fine.

I think my induction troubles are solved with that. Still would be nice to get default attributes, though.



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