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.blanche...@inria.fr> > wrote: > > Hi Gerwin, > >> On 19.04.2015, at 16:45, Gerwin Klein <gerwin.kl...@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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
