Re: [isabelle] Semantic hyperlinks: Hooray!

Offset references are "internal" references that are not captured in the foundational content. They should usually not be referred to from the outside, and are not stable w.r.t. to changes in a theory.

This happens inside a locale, as locale parameters are treated as free variables inside the context - but also, for instance, for named facts inside a proof.


On 11/11/21 00:11, Pedro Sánchez Terraf wrote:

On 7/11/21 16:38, Makarius wrote:
Dear Isabelle users,

please see and
for further progress on the release process.

The most notable change is HTML presentation with support for semantic hyperlinks!

This is great! Thank you very much for this update.

I've noted that the generated HTML has two kinds of links: one that points to something like


and the second kind points to


with XXXX and YYYY integers. The last kind seem to appear for items declared inside a locale. Is this the reason of the difference?

Pedro Sánchez Terraf
CIEM-FAMAF — Universidad Nacional de Córdoba
Moreover, there are some improvements of Poly/ML on native ARM64, but it is
still not finished.

Any feedback about release candidates should be posted with a meaningful
Subject (not just a clone of the announcement).


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