forked from Isabelle_DOF/Isabelle_DOF
typos, and a more general abstract.
This commit is contained in:
parent
032a9e9278
commit
7aefbde58b
|
@ -37,7 +37,9 @@ text*[abs::abstract,
|
|||
\<open> \isadof provides an implementation of \dof on top of Isabelle/HOL.
|
||||
\dof itself is a novel framework for \<^emph>\<open>defining\<close> ontologies
|
||||
and \<^emph>\<open>enforcing\<close> them during document development and document
|
||||
evolution. A major goal of \dof is the integrated development of
|
||||
evolution. \isadof targets use-cases such as mathematical texts referring
|
||||
to a theory development or technical reports requiring a particular structure.
|
||||
A major application of \dof is the integrated development of
|
||||
formal certification documents (\eg, for Common Criteria or CENELEC
|
||||
50128) that require consistency across both formal and informal
|
||||
arguments.
|
||||
|
@ -45,10 +47,14 @@ text*[abs::abstract,
|
|||
\isadof is integrated into Isabelle's IDE, which
|
||||
allows for smooth ontology development as well as immediate
|
||||
ontological feedback during the editing of a document.
|
||||
Its checking facilities leverage the collaborative
|
||||
development of documents required to be consistent with an
|
||||
underlying ontological structure.
|
||||
|
||||
In this paper, we give an in-depth presentation of the design
|
||||
concepts of \dof's Ontology Definition Language (ODL) and key
|
||||
aspects of the technology of its implementation. \isadof is the
|
||||
In this user-manual, we give an in-depth presentation of the design
|
||||
concepts of \dof's Ontology Definition Language (ODL) and describe
|
||||
comprehensively its major commands. Many examples show typical best-practice
|
||||
applications of the system. \isadof is the
|
||||
first ontology language supporting machine-checked
|
||||
links between the formal and informal parts in an LCF-style
|
||||
interactive theorem proving environment.
|
||||
|
|
|
@ -350,7 +350,7 @@ text\<open>
|
|||
characters in definitions that need to make use of a entries in an aux-file.
|
||||
\<close>
|
||||
|
||||
subsubsection\<open>Common Ontology Library (COL)\<close>
|
||||
subsection\<open>Common Ontology Library (COL)\<close>
|
||||
|
||||
text\<open>\isadof uses the concept of implicit abstract classes (or: \emph{shadow classes}).
|
||||
These refer to the set of possible \inlineisar+doc_class+ declarations that posses a number
|
||||
|
@ -359,7 +359,7 @@ of attributes with their types in common. Shadow classes represent an implicit r
|
|||
for certain \isadof commands.
|
||||
|
||||
shadow classes will find concrete instances in COL, but \isadof text elements do not \emph{depend}
|
||||
on our COL definitions: Ontology developers are free to use to build own instances for these
|
||||
on our COL definitions: Ontology developers are free to build own class instances for these
|
||||
shadow classes, with own attributes and, last not least, own definitions of invariants independent
|
||||
from ours.
|
||||
|
||||
|
|
|
@ -1,16 +1,3 @@
|
|||
(*************************************************************************
|
||||
* Copyright (C)
|
||||
* 2019 The University of Exeter
|
||||
* 2018-2019 The University of Paris-Saclay
|
||||
* 2018 The University of Sheffield
|
||||
*
|
||||
* License:
|
||||
* This program can be redistributed and/or modified under the terms
|
||||
* of the 2-clause BSD-style license.
|
||||
*
|
||||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
*************************************************************************)
|
||||
|
||||
structure RegExpChecker : sig
|
||||
type 'a equal
|
||||
type num
|
||||
|
|
Loading…
Reference in New Issue