[isabelle-dev] docs for new datatype package

[Gerwin Klein]

> 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.

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.