diff --git a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy
index 7acdcf5e..6988d674 100755
--- a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy
+++ b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy
@@ -119,10 +119,17 @@ text\<open>
       G.~Sala{\"u}n, editors, \<^emph>\<open>Software Engineering and Formal Methods (SEFM)\<close>, number 11724 in
       Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019.
       \href{https://doi.org/10.1007/978-3-030-30446-1_15}{10.1007/978-3-030-30446-1\_15}.
-
     \end{quote}
     A \<^BibTeX>-entry is available at: 
     \<^url>\<open>https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelledof-2019\<close>.
+  \<^item> for an application of \<^isadof> in the context of certifications:
+    \begin{quote}\small
+     A.~D. Brucker and B.~Wolff.
+     Using Ontologies in Formal Developments Targeting Certification. 
+     In W. Ahrendt and S. Tarifa, editors. \<^emph>\<open>Integrated Formal Methods (IFM)\<close>, number 11918.
+     Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019.
+     \href{https://doi.org/10.1007/978-3-030-34968-4\_4}.
+    \end{quote}
 \<close>
 subsubsection\<open>Availability\<close>
 text\<open>
diff --git a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy
index dc49930e..fce573bc 100755
--- a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy
+++ b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy
@@ -43,11 +43,11 @@ The current system framework offers moreover the following features:
 \<^item> an extensible front-end language Isabelle/Isar, and,
 \<^item> last but not least, an LCF style, generic theorem prover kernel as 
   the most prominent and deeply integrated system component.
-
-
+\<close>
+text\<open>
 The Isabelle system architecture shown in @{docitem \<open>architecture\<close>} comes with many layers, 
 with Standard ML (SML) at the bottom layer as implementation  language. The architecture actually 
-foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure\<^boxed_sml>\<open>Context\<close>. 
+foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure \<^boxed_sml>\<open>Context\<close>. 
 This structure provides a kind of container called \<^emph>\<open>context\<close> providing an identity, an 
 ancestor-list as well as typed, user-defined state for components (plugins) such as \<^isadof>. 
 On top of the latter, the LCF-Kernel, tactics,  automated proof procedures as well as specific 
diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex
index 7f4e4bf9..587f903c 100755
--- a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex
+++ b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex
@@ -41,8 +41,8 @@
 \pagestyle{headings}
 
 \uppertitleback{
-Copyright \copyright{} 2019--2021 University of Exeter, UK\\
-\phantom{Copyright \copyright{}} 2018--2021 Universit\'e Paris-Saclay, France\\
+Copyright \copyright{} 2019--2022 University of Exeter, UK\\
+\phantom{Copyright \copyright{}} 2018--2022 Universit\'e Paris-Saclay, France\\
 \phantom{Copyright \copyright{}} 2018--2019 The University of Sheffield, UK\\
 
 \smallskip
@@ -77,11 +77,13 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 
 \lowertitleback{%
 This manual describes \isadof version \isadofversion.  The latest official 
-release is \isadoflatestversion{} (\href{https://doi.org/\isadoflatestdoi}{doi:\isadoflatestdoi}). The DOI \href{https://doi.org/\isadofgenericdoi}{\isadofgenericdoi} will allways point to the latest release.  The latest development version as well as official releases are available at 
+release is \isadoflatestversion{} (\href{https://doi.org/\isadoflatestdoi}{doi:\isadoflatestdoi}). 
+The DOI \href{https://doi.org/\isadofgenericdoi}{\isadofgenericdoi} will allways point to the latest 
+release.  The latest development version as well as official releases are available at 
 \url{\dofurl}.
 
 \paragraph*{Contributors.} We would like to thank the following contributors to \isadof 
-(in alphabetical order): Idir Ait-Sadoune, Paolo Crisafulli, Chantal Keller, and Nicolas M{\'e}ric.
+(in alphabetical order): Idir Ait-Sadoune, Paolo Crisafulli, and Nicolas M{\'e}ric.
 
 \paragraph*{Acknowledgments.} This work has been partially supported by IRT SystemX, Paris-Saclay, 
 France, and therefore granted with public funds of the Program ``Investissements d'Avenir.''
@@ -107,7 +109,7 @@ France, and therefore granted with public funds of the Program ``Investissements
   \hfill
   \begin{minipage}{8cm}
     \raggedleft\normalsize
-    Laboratoire en Recherche en Informatique (LRI)\\
+    Laboratoire des Methodes Formelles (LMF)\\
     Universit\'e Paris-Saclay\\
     91405 Orsay Cedex\\
     France