Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

changed finish intro

This commit is contained in:
Burkhart Wolff 2022-04-20 13:57:32 +02:00
parent 53333d7096
commit 8e056e0e8a
1 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -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.\<close>
(*<*)