diff --git a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy index 3f98ca3..9899d95 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy @@ -37,7 +37,9 @@ text*[abs::abstract, \ \isadof provides an implementation of \dof on top of Isabelle/HOL. \dof itself is a novel framework for \<^emph>\defining\ ontologies and \<^emph>\enforcing\ 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. diff --git a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy index b7096af..eb68c01 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy @@ -42,11 +42,11 @@ In general, an ontology is a formal explicit description of \<^emph>\conce as \<^emph>\links\ between them. A particular link between concepts is the \<^emph>\is-a\ relation declaring the instances of a subclass to be instances of the super-class. -To adress this challenge, we present developed the Document Ontology Framework (\dof). \dof is -designed for building scalable and user-friendly tools on top of interactive theorem provers, -and an implementation of DOF called \isadof. \isadof is a novel framework, extending of +To adress this challenge, we present the Document Ontology Framework (\dof) and an +implementation of DOF called \isadof. \dof is designed for building scalable and user-friendly +tools on top of interactive theorem provers. \isadof is a novel framework, implemented as extension of Isabelle/HOL, to \<^emph>\model\ typed ontologies and to \<^emph>\enforce\ them during document evolution. Based -on Isabelle infrastructures, ontologies may refer to types, terms, proven theorems, code, or +on Isabelle's infrastructures, ontologies may refer to types, terms, proven theorems, code, or established assertions. Based on a novel adaption of the Isabelle IDE, a document is checked to be \<^emph>\conform\ to a particular ontology---\isadof is designed to give fast user-feedback \<^emph>\during the capture of content\. This is particularly valuable in case of document evolution, where the @@ -124,8 +124,8 @@ text\ \<^item> for the implementation of \isadof~@{cite "brucker.ea:isabelledof:2019"}: \begin{quote}\small A.~D. Brucker and B.~Wolff. \isadof: Design and implementation. In P.~{\"O}lveczky and - G.~Sala{\"u}n, editors, \<^emph>\Software Engineering and Formal Methods (SEFM)\, Lecture Notes - in Computer Science. Springer-Verlag, Heidelberg, 2019. + G.~Sala{\"u}n, editors, \<^emph>\Software Engineering and Formal Methods (SEFM)\, number 11724 in + Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019. \end{quote} A \BibTeX-entry is available at: \url{https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelledof-2019}. diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 539e834..f67b3cd 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -350,7 +350,7 @@ text\ characters in definitions that need to make use of a entries in an aux-file. \ -subsubsection\Common Ontology Library (COL)\ +subsection\Common Ontology Library (COL)\ text\\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. diff --git a/src/DOF/RegExpChecker.sml b/src/DOF/RegExpChecker.sml index d74a947..404d741 100644 --- a/src/DOF/RegExpChecker.sml +++ b/src/DOF/RegExpChecker.sml @@ -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