> On 21 Apr 2015, at 6:07 pm, Jasmin Blanchette <jasmin.blanche...@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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
