[isabelle-dev] docs for new datatype package

Gerwin Klein Gerwin.Klein at nicta.com.au
Sun Apr 19 20:25:24 CEST 2015

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?


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

More information about the isabelle-dev mailing list