diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/preamble.tex b/examples/scholarly_paper/2021-ITP-PMTI/document/preamble.tex
index 38c30447..0a30851f 100644
--- a/examples/scholarly_paper/2021-ITP-PMTI/document/preamble.tex
+++ b/examples/scholarly_paper/2021-ITP-PMTI/document/preamble.tex
@@ -2,6 +2,8 @@
\usepackage{stmaryrd}
+\newcommand{\acs}[1]{}
+
\title{
}
\author{}
diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib
index 6b3f479d..771ccaa1 100644
--- a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib
+++ b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib
@@ -48,6 +48,41 @@ code generation.",
isbn="978-3-319-96812-4"
}
+@Misc{w3c:ontologies:2015,
+ title={Ontologies},
+ organisation={W3c},
+ url={https://www.w3.org/standards/semanticweb/ontology},
+ year=2018
+}
+
+@BOOK{boulanger:cenelec-50128:2015,
+ AUTHOR = "Boulanger, Jean-Louis",
+ TITLE = "{CENELEC} 50128 and {IEC} 62279 Standards",
+ PUBLISHER = "Wiley-ISTE",
+ YEAR = "2015",
+ ADDRESS = "Boston",
+ NOTE = "The reference on the standard."
+}
+
+@Booklet{ cc:cc-part3:2006,
+ bibkey = {cc:cc-part3:2006},
+ key = {Common Criteria},
+ institution = {Common Criteria},
+ language = {USenglish},
+ month = sep,
+ year = 2006,
+ public = {yes},
+ title = {Common Criteria for Information Technology Security
+ Evaluation (Version 3.1), {Part} 3: Security assurance
+ components},
+ note = {Available as document
+ \href{http://www.commoncriteriaportal.org/public/files/CCPART3V3.1R1.pdf}
+ {CCMB-2006-09-003}},
+ number = {CCMB-2006-09-003},
+ acknowledgement={brucker, 2007-04-24}
+}
+
+
@article{DBLP:journals/jcs/RoscoeB99,
author = {A. W. Roscoe and
Philippa J. Broadfoot},
@@ -2630,23 +2665,6 @@ isbn="978-3-540-48509-4"
acknowledgement={brucker, 2007-04-23}
}
-@Booklet{ cc:cc-part3:2006,
- bibkey = {cc:cc-part3:2006},
- key = {Common Criteria},
- institution = {Common Criteria},
- language = {USenglish},
- month = sep,
- year = 2006,
- public = {yes},
- title = {Common Criteria for Information Technology Security
- Evaluation (Version 3.1), {Part} 3: Security assurance
- components},
- note = {Available as document
- \href{http://www.commoncriteriaportal.org/public/files/CCPART3V3.1R1.pdf}
- {CCMB-2006-09-003}},
- number = {CCMB-2006-09-003},
- acknowledgement={brucker, 2007-04-24}
-}
@Booklet{ omg:ocl:1997,
bibkey = {omg:ocl:1997},
diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy
index 5aa42ca2..756e602f 100644
--- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy
+++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy
@@ -14,6 +14,8 @@ declare[[ Theorem_default_class = "theorem"]]
define_shortcut* hol \ \HOL\
isabelle \ \Isabelle/HOL\
dof \ \Isabelle/DOF\
+ latex \ \LaTeX\
+ html \ \HTML\
csp \ \CSP\ \\obsolete\
holcsp \ \HOL-CSP\ \\obsolete\
@@ -42,10 +44,76 @@ abstract*[abs, keywordlist="[\Ontologies\,\Formal Documents\<
and specific ontology instances in concrete cases. This concept is also called
\<^emph>\ontology alignment\ in the literature raised a substantial interest recently.
\
-text\\
-section*[introheader::introduction,main_author="Some(@{docitem ''bu''}::author)"]\ Introduction \
+
+section*[introheader::introduction,main_author="Some(@{docitem ''bu''}::author)"]\ Introduction \
text*[introtext::introduction]\
-THE FOLLOWING IS STILL RUBBISH AND JUST SHOWS HOW TO WRITE A PAPER IN ISABELLE-DOF.
+The linking of \<^emph>\formal\ and \<^emph>\informal\ information is perhaps the
+most pervasive challenge in the digitization of knowledge and its
+propagation. This challenge incites numerous research efforts
+summarized under the labels ``semantic web'', ``data mining'', or any
+form of advanced ``semantic'' text processing. Turning informal into
+(more) formal content is the key for advanced techniques of research,
+combination, and the maintenance of consistency in the midst of data evolution.
+
+Admittedly, Isabelle is not the first system that comes into one's mind when
+writing a document, be it a scientific paper, a book, or a larger technical
+documentation. However, it has a typesetting system inside which is in the
+tradition of document generation systems such as mkd, Document! X, Doxygen,
+Javadoc, etc., which embed elements of formal content such as code-snippets
+or generated system output into informal text. In Isabelle, these "embedders"
+or meta-text elements are a form of machine-checked macro called \<^emph>\antiquotations\.
+
+For example, the text element as appearing in the Isabelle frontend:
+@{theory_text [display]
+ \ According to the reflexivity axiom @{thm refl}, we obtain in \
+ for @{term "fac 5"} the result @{value "fac 5"}.\}
+is represented in the generated LaTeX or HTML output by:
+@{theory_text [display]
+ \According to the reflexivity axiom \x = x\, we obtain in \ for \fac 5\ the result \120\.\
+}
+where the meta-texts \@{thm refl}\ ("give the presentation of theorem 'refl'),
+\@{term "fac 5"}\ ("parse and type-check 'fac 5' in the previous logical context)
+and \@{value "fac 5"}\ ("compile and execute 'fac 5' according to its
+definitions in the previous logical context) are built-in antiquotations
+in \<^hol>.
+
+
+
+
+ A key role in
+structuring this linking play \<^emph>\document ontologies\ (also called
+\<^emph>\vocabulary\ in the semantic web community~@{cite "w3c:ontologies:2015"}),
+\<^ie>, a machine-readable form of the structure of data as well as
+the discourse.
+
+Such ontologies can be used for the scientific discourse within scholarly
+articles, mathematical libraries, and in the engineering discourse
+of standardized software certification
+documents~@{cite "boulanger:cenelec-50128:2015" and "cc:cc-part3:2006"}.
+Further applications are the domain-specific discourse in juridical texts or medical reports.
+In general, an ontology is a formal explicit description of \<^emph>\concepts\
+in a domain of discourse (called \<^emph>\classes\), properties of each concept
+describing \<^emph>\attributes\ of the concept, as well 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.
+
+The main objective of this paper is to present \<^dof>, a novel
+framework 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 established assertions.
+Based on a novel adaption of the Isabelle IDE, a document is checked to be
+\<^emph>\conform\ to a particular ontology---\<^dof> is designed to give fast user-feedback
+\<^emph>\during the capture of content\. This is particularly valuable in case of document
+changes, where the \<^emph>\coherence\ between the formal and the informal parts of the
+content can be mechanically checked.
+
+To avoid any misunderstanding: \<^dof> is \<^emph>\not a theory in HOL\
+on ontologies and operations to track and trace links in texts,
+it is an \<^emph>\environment to write structured text\ which \<^emph>\may contain\
+\<^isabelle> definitions and proofs like mathematical articles, tech-reports and
+scientific papers---as the present one, which is written in \<^dof>
+itself. \<^dof> is a plugin into the Isabelle/Isar
+framework in the style of~@{cite "wenzel.ea:building:2007"}.
Communicating Sequential Processes (\<^csp>) is a language
@@ -62,8 +130,7 @@ but has since evolved substantially @{cite "BrookesHR84" and "brookes-roscoe85"
\<^csp> describes the most common communication and synchronization mechanisms
with one single language primitive: synchronous communication written \_\_\_\. \<^csp> semantics is
described by a fully abstract model of behaviour designed to be \<^emph>\compositional\: the denotational
-semantics of a process \P\ encompasses all possible behaviours of this process in the context of all
-possible environments \P \S\ Env\ (where \S\ is the set of \atomic events\ both \P\ and \Env\ must
+semantics of a possible environments \P \S\ Env\ (where \S\ is the set of \atomic events\ both \P\ and \Env\ must
synchronize). This design objective has the consequence that two kinds of choice have to
be distinguished:
\<^enum> the \<^emph>\external choice\, written \_\_\, which forces a process "to follow" whatever