Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Document antiquotation for referring to lemmas

Email Gateway (Aug 23 2021 at 09:54):

From: Dominique Unruh <unruh@ut.ee>
Hello,

I was wondering whether there exists a document antiquotation for
referencing an existing lemma.

Something like: text ‹See lemma @{thm refl}›

Except that the above included the lemma content, not it's name. (I.e.,
it renders as /See lemma ?x=?x/. I want to see /See lemma refl./)

Of course, I can just write the lemma name verbatim (e.g., text ‹See
lemma ‹refl››) but that will not check whether the lemma exists etc.

(And as a related side-remark: It would be cool if in a future Isabelle
release, the document generation would add labels next to lemmas etc. So
that something like \ref{lemma:my_lemma_name} could jump to the lemma
declaration via hyperref.)

Best wishes,
Dominique.

Email Gateway (Aug 23 2021 at 12:48):

From: Makarius <makarius@sketis.net>
On 23/08/2021 11:53, Dominique Unruh wrote:

Something like: text ‹See lemma @{thm refl}›

You can do it like this, although it is a bit indirect and archaic:

@{thm [source] refl}

(And as a related side-remark: It would be cool if in a future Isabelle
release, the document generation would add labels next to lemmas etc. So that
something like \ref{lemma:my_lemma_name} could jump to the lemma declaration
via hyperref.)

Something like this has been in the pipeline for approx. 10 years. Eventually
it will be flushed, probably within 1-2 releases.

Makarius

Last updated: Jul 15 2022 at 23:21 UTC