nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

typo

This commit is contained in:
Burkhart Wolff 2022-02-08 23:13:08 +01:00
parent f1e01a5b86
commit a4708957d5
1 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
examples/scholarly_paper/2021-ITP-PMTI/paper.thy
View File

@ -1338,13 +1338,13 @@ of formal content, be it in the engineering or the mathematics domain.
\<^footnote>\<open>This paper has been edited in \<^dof>, of course.\<close> \<^footnote>\<open>This paper has been edited in \<^dof>, of course.\<close>
Another line of future application is to increase the ``depth'' of built-in term antiquotations such Another line of future application is to increase the ``depth'' of built-in term antiquotations such
as \<^theory_text>\<open>@{typ \<open>'\<tau>\<close>}\<close>, \<^term>\<open>@{term \<open>a + b\<close>}\<close> and \<^term>\<open>@{thm \<open>HOL.refl\<close>}\<close>, which are currently implemented just as as \<^theory_text>\<open>@{typ \<open>'\<tau>\<close>}\<close>, \<^term>\<open>@{term \<open>a + b\<close>}\<close> and \<^term>\<open>@{thm \<open>HOL.refl\<close>}\<close>, which are currently implemented
validations in the current logical context. In the future, they could optionally be expanded to just as validations in the current logical context. In the future, they could optionally be expanded
the types, terms and theorems (with proof objects attached) in a meta-model of the Isabelle Kernel 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). 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 This will allow for definitions of query-functions in, \<^eg>, proof-objects, and pave the way
pave the way to annotate them with typed meta-data. Such a technology could be relevant to annotate them with typed meta-data. Such a technology could be relevant for the interoperability
for the interoperability of proofs across different ITP platforms. of proofs across different ITP platforms.
\<close> \<close>
(*<*) (*<*)