如何在Isabelle文本中引用lemma/theorem/corollary的名称？

• 直接使用@{thm_name <目标名称>}这个document antiquotation就能满足所有需求：
  • 编译PDF时会显示对应的定理、引理或推论的名称
  • IDE中支持Ctrl点击跳转至目标声明的定义位置
  • 重命名目标实体时，引用会自动同步更新，彻底避免手动输入名称带来的维护问题

完整示例代码：

theory Scratch
  imports Main
begin

lemma lemma_name: "stuff = stuff" by simp

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

end

编译后的PDF会显示：As we have proven in fact lemma_name, stuff is stuff.，完全符合预期。

另外，@{thm_name}不仅适用于lemma，对theorem、corollary这类定理型实体也同样生效。

内容的提问来源于stack exchange，提问作者corny