From a4708957d512db6285292d08a524f5c4536fd4f4 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Tue, 8 Feb 2022 23:13:08 +0100 Subject: [PATCH] typo --- examples/scholarly_paper/2021-ITP-PMTI/paper.thy | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index 6e5666ec..e7ca740a 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -1338,13 +1338,13 @@ of formal content, be it in the engineering or the mathematics domain. \<^footnote>\This paper has been edited in \<^dof>, of course.\ Another line of future application is to increase the ``depth'' of built-in term antiquotations such -as \<^theory_text>\@{typ \'\\}\, \<^term>\@{term \a + b\}\ and \<^term>\@{thm \HOL.refl\}\, which are currently implemented just as -validations in the current logical context. In the future, they could optionally be expanded to -the types, terms and theorems (with proof objects attached) in a meta-model of the Isabelle Kernel +as \<^theory_text>\@{typ \'\\}\, \<^term>\@{term \a + b\}\ and \<^term>\@{thm \HOL.refl\}\, which are currently implemented +just as validations in the current logical context. In the future, they could optionally be expanded +to the types, terms and theorems (with proof objects attached) in a meta-model of the Isabelle Kernel such as the one presented in @{cite "10.1007/978-3-030-79876-5_6"} (also available in the AFP). -This will allow for specifications of query-functions in, \<^eg>, proof-objects, and -pave the way to annotate them with typed meta-data. Such a technology could be relevant -for the interoperability of proofs across different ITP platforms. +This will allow for definitions of query-functions in, \<^eg>, proof-objects, and pave the way +to annotate them with typed meta-data. Such a technology could be relevant for the interoperability +of proofs across different ITP platforms. \ (*<*)