[isabelle-dev] docs for new datatype package

[Gerwin Klein]

Thanks for updating.

Currently trying to pull through proofs in https://github.com/seL4/l4v/blob/master/tools/c-parser/umm_heap/CTypes.thy

They are unfortunately pretty horrid to start with (violating half of our own style/maintenance rules), additionally contain lots of nested recursion and some proofs about size_t functions that seem to have changed quite a bit. I’m tempted to use old_datatype here.

How long did we plan on keeping the old datatype package around?

Cheers,
Gerwin

> On 19 Apr 2015, at 6:48 pm, Jasmin Blanchette <jasmin.blanchette at inria.fr> wrote:
>
> Hi Gerwin,
>
>> On 19.04.2015, at 16:45, Gerwin Klein <Gerwin.Klein at nicta.com.au> wrote:
>>
>> 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?
>
> Indeed, this is a couple of versions behind. Skimming through the document, I found a few other obsolete remarks (852f7a49ec0c).
>
> Thanks!
>
> Jasmin
>


________________________________

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.