From 8e056e0e8a3670e42d752e3117544c89255384c1 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Wed, 20 Apr 2022 13:57:32 +0200 Subject: [PATCH] changed finish intro --- examples/scholarly_paper/2021-ITP-PMTI/paper.thy | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index cffc9e3..e78e69c 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -254,8 +254,9 @@ for advanced queries of elements inside an integrated source, and invariants allow for formal proofs over the relations/translations of ontologies and ontology-instances. The latter question raised scientific interest under the label ``ontology mapping'' for which we therefore present a formal solution. To sum up, we completed \<^dof> to -a fairly rich, ITP-oriented ontology language, which is a concrete proposal for the -ITP community allowing a deeper structuring of mathematical libraries +a fairly rich, ITP-oriented ontology language, which is a concrete proposal for formal +development projects targeting a certification, for technical documentation or books +with a high amount of machine-checked formal content or for mathematical libraries such as the AFP.\ (*<*)