Revised abstract.

examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy

@@ -18,28 +18,29 @@ text*[bu::author,
       email       = "\<open>wolff@lri.fr\<close>",
       affiliation = "\<open>Université Paris-Saclay, LRI, Paris, France\<close>"]\<open>Burkhart Wolff\<close>
  
-
 text*[abs::abstract,
-      keywordlist="[''Ontology'',''Ontological Modeling'',''Isabelle/DOF'']"]\<open>
-While Isabelle is mostly known as part of Isabelle/HOL (an interactive 
-theorem prover), it actually provides a framework for developing a wide
-spectrum of applications. A particular strength
-of the Isabelle framework is the combination of text editing, formal verification,
-and code generation. 
+      keywordlist="[''Ontology'', ''Ontological Modeling'', ''Document Management'', 
+                    ''Formal Document Development'', ''Document Authoring'', ''Isabelle/DOF'']"]
+\<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
+  formal certification documents (\eg, for Common Criteria or CENELEC
+  50128) that require consistency across both formal and informal
+  arguments.
 
-Up to now, Isabelle's document preparation system lacks a mechanism
-for ensuring the structure of different document types (as, e.g.,
-required in certification processes) in general and, in particular,
-a \<^emph>\<open>systematic\<close> mechanism for linking informal and formal parts of a document. 
-
-In this paper, we present \isadof, a novel Document Ontology Framework 
-on top of Isabelle. \isadof allows for conventional typesetting
-\<^emph>\<open>as well\<close> as formal development. We show how to model document
- ontologies inside \isadof, how to use the resulting meta-information 
-for enforcing a certain document structure, and discuss ontology-specific IDE support. 
+  \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.
+  
+  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
+  first ontology language supporting machine-checked
+  links between the formal and informal parts in an LCF-style
+  interactive theorem proving environment.
 \<close>
 
-
 (*<*) 
 end
 (*>*)