Re: [isabelle] Isabelle2016-RC0 - isar-ref.pdf datatype documentation

Hi Cornelius,

> when I'm looking for datatypes in the table of contents of isar-ref, I
> can only find "11.5 Old-style datatypes".
> The section only tells:
> "These commands are mostly obsolete; datatype should be used instead.
> See [35] for more details on datatypes, but beware of the old-style theory syn-
> tax being used there!"
> [35] T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelleâs Logics: HOL.
> The link in [35] is 404.

Thank you for your report. I have prepared a changeset to point to the right documentation ("isabelle doc datatypes"). Makarius, please apply the attached changset patch to "isabelle-release".

I took out two references to "isabelle-hol", but there are two left in the tutorial. I'm not sure what happened to this document and/or why there are still broken references to it, but I'd rather leave the tutorial authors fix it.



Attachment: hol_spec.export
Description: Binary data

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.