From 7aefbde58b51434358b52cbdcfb601730f8187cf Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Sat, 17 Aug 2019 10:23:16 +0200
Subject: [PATCH] typos, and a more general abstract.

---
 .../Isabelle_DOF-Manual/00_Frontmatter.thy         | 14 ++++++++++----
 .../Isabelle_DOF-Manual/04_RefMan.thy              |  4 ++--
 src/DOF/RegExpChecker.sml                          | 13 -------------
 3 files changed, 12 insertions(+), 19 deletions(-)

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,
 \<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.
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\<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.
 
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