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.


Fabian

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

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

please see https://isabelle.sketis.net/website-Isabelle2021-1-RC2 and
https://isabelle-dev.sketis.net/phame/post/view/53/release_candidates_for_isabelle2021-1
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

  #Theory.item|type

and the second kind points to

  #offset_XXXX_YYYY

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
cs.famaf.unc.edu.ar/~pedro
 
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).


	Makarius




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