[isabelle-dev] docs for new datatype package

Jasmin Blanchette jasmin.blanchette at inria.fr
Sun Apr 19 19:48:26 CEST 2015

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



More information about the isabelle-dev mailing list