Search code examples
isabelle

Print the name of a fact in a document antiquotation

Can I somehow refer to the name of a lemma (or theorem or corollary) inside Isabelle text?

For example:

theory Scratch
  imports Main
begin

lemma lemma_name: "stuff = stuff" by simp

text‹As we have proven in fact @{thm lemma_name}, stuff is stuff.›

end

When compiling this to pdf, I see

As we have proven in fact stuff=stuff, stuff is stuff.

I would like to see

As we have proven in fact lemma_name, stuff is stuff.

Is there some document antiqotation which just prints the name of a lemma?

I could just type the lemma name verbatim, but this neither gives me control-click in the IDE nor does it make sure the text still refers to a true fact, even if I rename lemmas.

Solution

  • The output of antiquotations can be changed by options explained in 4.2.1 and 4.2.2 of the Isabelle/Isar Reference Manual. One (rather hidden) option [source=true] sets the output to print what you have entered as argument to the antiquotation instead of its output.

    text ‹As we have proven in fact @{thm [source] lemma_name}, stuff is stuff.

    ...will thus result in the document output:

    As we have proven in fact lemma_name, stuff is stuff.

    The checking of the validity of the reference will still take place during document preparation.