Email Gateway (Nov 10 2021 at 23:12): Email Gateway (Nov 10 2021 at 23:12):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
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?
Email Gateway (Nov 11 2021 at 07:59):From: Fabian Huch <huch@in.tum.de>
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
Last updated: Jan 04 2025 at 20:18 UTC