diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index 3507e666..3766b96e 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -165,7 +165,7 @@ and typed reference mechanisms inside text- and ML-contexts. *) -text\In this paper, we extend prior versions of \<^dof> by +text\As novel contribution, this work extends prior versions of \<^dof> by \<^enum> support of antiquotions in a new class of contexts, namely \<^emph>\term contexts\ (rather than SML code or semi-formal text). Thus, annotations generated from \<^dof> may also occur in \\\-terms used to denote meta-data. @@ -174,13 +174,13 @@ text\In this paper, we extend prior versions of \<^dof> by common HOL \\\-term syntax. \ text\ For example, the \<^dof> evaluation command taking a HOL-expression: -@{theory_text [display,indent=10, margin=70] -\ value*[ass::Assertion, relev=2::int] \mapfilter (\ \. relev \ > 2) @{instance_of \Assertion\}\\ +@{theory_text [display,indent=6, margin=70] +\ value*[ass::Assertion, relvce=2::int] \mapfilter (\ \. relvce \ > 2) @{instance_of \Assertion\}\\ } where \<^dof> command \value*\ type-checks, expands in an own validation phase the \instance_of\-term antiquotation, and evaluates the resulting HOL expression above. Assuming an ontology providing the class \Assertion\ having at least the -integer attribute \relev\, the command finally creates an instance of \Assertion\ and +integer attribute \relvce\, the command finally creates an instance of \Assertion\ and binds this to the label \ass\ for further use. Beyond the gain of expressivity in \<^dof> ontologies, term-antiquotations pave the way