[isabelle-dev] docs for new datatype package
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