diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index 3adefc4d..a9ee5764 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -651,7 +651,7 @@ declare_reference*["term-context-equality-evaluation"::figure] (*>*) text\ - We can even compare classes. \<^figure>\term-context-equality-evaluation\ + We can even compare class instances. \<^figure>\term-context-equality-evaluation\ shows that the two class instances \<^theory_text>\resultProof\ and \<^theory_text>\resultProof2\ are not equivalent because their attribute \<^theory_text>\property\ differ. \