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.
> http://isabelle.in.tum.de/doc/logics-HOL.pdf.
> 
> 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.

Cheers,

Jasmin

Attachment: hol_spec.export
Description: Binary data



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