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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
