Test 2022 phd poster generation

examples/scholarly_paper/2022-phd-poster/ROOT

@@ -0,0 +1,26 @@
+session "2022-phd-poster" = "Isabelle_DOF" +
+  options [document = pdf, document_output = "output", document_build = dof,
+    document_comment_latex = true]
+  theories
+    "paper"
+  document_files
+    "isadof.cfg"
+    "root.bib"
+    "preamble.tex"
+    "lstisadof.sty"
+    "figures/afp_growth_in_number_of_articles.png"
+    "figures/classes_with_invariant.png"
+    "figures/code_antiquotations.png"
+    "figures/dof_classes.png"
+    "figures/dof_document.png"
+    "figures/invariant_preserved.png"
+    "figures/local_ontology.png"
+    "figures/morphism.png"
+    "figures/odl.png"
+    "figures/ontological_context.png"
+    "figures/output.png"
+    "figures/reference_ontology.png"
+    "figures/sml_code_with_antiquotations.png"
+    "figures/text_element.png"
+    "figures/text_element_with_formal_content.png"
+    "figures/theories_hierarchy.png"

examples/scholarly_paper/2022-phd-poster/document/isadof.cfg

@@ -0,0 +1,2 @@
+Template: 2022-phd-poster
+Ontology: scholarly_paper

examples/scholarly_paper/2022-phd-poster/document/lstisadof.sty

@@ -0,0 +1,195 @@
+%% Copyright (C) 2018 The University of Sheffield
+%%               2018 The University of Paris-Saclay
+%%               2019 The University of Exeter
+%%
+%% License:
+%%   This program can be redistributed and/or modified under the terms
+%%   of the LaTeX Project Public License Distributed from CTAN
+%%   archives in directory macros/latex/base/lppl.txt; either
+%%   version 1.3c of the License, or (at your option) any later version.
+%%   OR
+%%   The 2-clause BSD-style license.
+%%
+%%   SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
+\usepackage{listings}
+\usepackage{listingsutf8}
+\usepackage{tikz}
+\usepackage[many]{tcolorbox}
+\tcbuselibrary{listings}
+\tcbuselibrary{skins}
+\usepackage{xstring}
+
+\definecolor{OliveGreen}    {cmyk}{0.64,0,0.95,0.40}
+\definecolor{BrickRed}      {cmyk}{0,0.89,0.94,0.28}
+\definecolor{Blue}          {cmyk}{1,1,0,0}
+\definecolor{CornflowerBlue}{cmyk}{0.65,0.13,0,0}
+
+%%%\lst@BeginAspect[keywords]{isar}
+\gdef\lst@tagtypes{s}
+\gdef\lst@TagKey#1#2{%
+    \lst@Delim\lst@tagstyle #2\relax
+        {Tag}\lst@tagtypes #1%
+                     {\lst@BeginTag\lst@EndTag}%
+        \@@end\@empty{}}
+\lst@Key{tag}\relax{\lst@TagKey\@empty{#1}}
+\lst@Key{tagstyle}{}{\def\lst@tagstyle{#1}}
+\lst@AddToHook{EmptyStyle}{\let\lst@tagstyle\@empty}
+\gdef\lst@BeginTag{%
+    \lst@DelimOpen
+        \lst@ifextags\else
+        {\let\lst@ifkeywords\iftrue
+         \lst@ifmarkfirstintag \lst@firstintagtrue \fi}}
+\lst@AddToHookExe{ExcludeDelims}{\let\lst@ifextags\iffalse}
+\gdef\lst@EndTag{\lst@DelimClose\lst@ifextags\else}
+\lst@Key{usekeywordsintag}t[t]{\lstKV@SetIf{#1}\lst@ifusekeysintag}
+\lst@Key{markfirstintag}f[t]{\lstKV@SetIf{#1}\lst@ifmarkfirstintag}
+\gdef\lst@firstintagtrue{\global\let\lst@iffirstintag\iftrue}
+\global\let\lst@iffirstintag\iffalse
+ \lst@AddToHook{PostOutput}{\lst@tagresetfirst}
+ \lst@AddToHook{Output}
+     {\gdef\lst@tagresetfirst{\global\let\lst@iffirstintag\iffalse}}
+ \lst@AddToHook{OutputOther}{\gdef\lst@tagresetfirst{}}
+\lst@AddToHook{Output}
+    {\ifnum\lst@mode=\lst@tagmode
+         \lst@iffirstintag \let\lst@thestyle\lst@gkeywords@sty \fi
+         \lst@ifusekeysintag\else \let\lst@thestyle\lst@gkeywords@sty\fi
+     \fi}
+\lst@NewMode\lst@tagmode
+\gdef\lst@Tag@s#1#2\@empty#3#4#5{%
+    \lst@CArg #1\relax\lst@DefDelimB {}{}%
+        {\ifnum\lst@mode=\lst@tagmode \expandafter\@gobblethree \fi}%
+        #3\lst@tagmode{#5}%
+    \lst@CArg #2\relax\lst@DefDelimE {}{}{}#4\lst@tagmode}%
+\gdef\lst@BeginCDATA#1\@empty{%
+    \lst@TrackNewLines \lst@PrintToken
+    \lst@EnterMode\lst@GPmode{}\let\lst@ifmode\iffalse
+    \lst@mode\lst@tagmode #1\lst@mode\lst@GPmode\relax\lst@modetrue}
+%%\lst@EndAspect
+
+
+
+% \gdef\lst@BeginTag{%
+%     \lst@DelimOpen
+%     \lst@ifextags\else
+%         {\let\lst@ifkeywords\iftrue
+%          \lst@ifmarkfirstintag\lst@firstintagtrue\fi\color{green}}}
+% \gdef\lst@EndTag{\lst@DelimClose\lst@ifextags\else\color{green}}
+
+\def\beginlstdelim#1#2#3%
+{%
+    \def\endlstdelim{\texttt{\textbf{\color{black!60}#2}}\egroup}%
+    \ttfamily\textbf{\color{black!60}#1}\bgroup\rmfamily\color{#3}\aftergroup\endlstdelim%
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% <isar>
+\providecolor{isar}{named}{gray}
+%\renewcommand{\isacommand}[1]{\textcolor{OliveGreen!60}{\ttfamily\bfseries #1}}
+\newcommand{\inlineisarbox}[1]{#1}
+\NewTColorBox[]{isarbox}{}{
+     ,boxrule=0pt
+     ,boxsep=0pt
+     ,colback=white!90!isar
+     ,enhanced jigsaw
+     ,borderline west={2pt}{0pt}{isar!60!black}
+     ,sharp corners
+     ,before skip balanced=0.5\baselineskip plus 2pt
+     % ,before skip=10pt
+     % ,after skip=10pt
+     ,enlarge top by=0mm
+     ,enhanced
+     ,overlay={\node[draw,fill=isar!60!black,xshift=0pt,anchor=north
+       east,font=\bfseries\footnotesize\color{white}]
+                at (frame.north east) {Isabelle code};}
+}
+%% </isar>
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\newcommand{\subscr}[1]{\ensuremath{_{\mbox{#1}}}}
+\newcommand{\supscr}[1]{\ensuremath{^{\mbox{#1}}}}
+\lstdefinestyle{ISAR}{%
+  language=%
+  ,basicstyle=\ttfamily%
+  ,showspaces=false%
+  ,showlines=false%
+  ,columns=flexible%
+  ,morecomment=[s]{(*}{*)}%
+  % ,moredelim=*[s][\rmfamily]{\{*}{*\}}%
+  ,moredelim = **[is][\beginlstdelim{\{*}{*\}}{black}]{\{*}{*\}}
+  ,showstringspaces=false%
+  ,moredelim=*[is][\supscr]{\\<^bsup>}{\\<^esup>}%
+  ,literate={%
+    {...}{\,\ldots\,}3%
+    {\\<Open>}{\ensuremath{\isacartoucheopen}}1%
+    {\\at}{@}1%
+    {\\<Close>}{\ensuremath{\isacartoucheclose}}1%
+    {\\<Gamma>}{\ensuremath{\Gamma}}1%
+    {\\<times>}{\ensuremath{\times}}1%
+    {\\<rbrakk>}{\ensuremath{\mathclose{\rbrack\mkern-3mu\rbrack}}}1%
+    {\\<rbrace>}{\ensuremath{\mathclose{\mid\mkern-4.5mu\rbrace}}}1%
+    {\\<lbrakk>}{\ensuremath{\mathopen{\lbrack\mkern-3mu\lbrack}}}1%
+    {\\<lbrace>}{\ensuremath{\mathopen{\lbrace\mkern-4.5mu\mid}}}1%
+    {\\<Rightarrow>}{\ensuremath{\Rightarrow}}1%
+    {\{*}{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}1%
+    {*\}}{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}1%
+  }%
+  % % Defining "tags" (text-antiquotations) based on 1-keywords
+   ,tag=**[s]{@\{}{\}}%
+   ,tagstyle=\color{CornflowerBlue}%
+   ,markfirstintag=true%
+   ,keywordstyle=\bfseries%
+   ,keywords={}
+   % Defining 2-keywords
+   ,keywordstyle=[2]{\color{Blue!60}\bfseries}%
+   ,alsoletter={*,-}
+   ,morekeywords=[2]{theory, begin, end, ML,section,subsection,paragraph,chapter,text}%
+   %,moredelim=[s][\textit]{<}{>}
+   % Defining 3-keywords
+   ,keywordstyle=[3]{\color{OliveGreen!60}\bfseries}%
+   ,morekeywords=[3]{doc_class,declare_reference,update_instance*,
+     open_monitor*, close_monitor*, figure*, title*, subtitle*,declare_reference*,section*,text*}%
+   % Defining 4-keywords
+   ,keywordstyle=[4]{\color{black!60}\bfseries}%
+   ,morekeywords=[4]{where, imports}%
+   % Defining 5-keywords
+   ,keywordstyle=[5]{\color{BrickRed!70}\bfseries}%
+   ,morekeywords=[5]{datatype, typedecl, consts, theorem}%
+   % Defining 6-keywords
+   ,keywordstyle=[6]{\itshape}%
+   ,morekeywords=[6]{meta-args, ref, expr, class_id}%
+  % 
+}%
+%% 
+\lstnewenvironment{isar}[1][]{\lstset{style=ISAR,
+    backgroundcolor=\color{black!2},
+    frame=lines,
+    mathescape=true,
+    basicstyle=\footnotesize\ttfamily,#1}}{}
+%%% 
+\def\inlineisar{\lstinline[style=ISAR,breaklines=true,mathescape,breakatwhitespace=true]}
+
+\lstnewenvironment{out}[1][]{\lstset{
+    backgroundcolor=\color{green!2},
+    frame=lines,mathescape,breakatwhitespace=true
+    ,columns=flexible%
+    ,basicstyle=\footnotesize\rmfamily,#1}}{}
+
+
+%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%
+\lstloadlanguages{ML}
+\lstdefinestyle{sml}{basicstyle=\ttfamily,%
+                     commentstyle=\itshape,%
+                     keywordstyle=\bfseries\color{CornflowerBlue},%
+                     ndkeywordstyle=\color{red},%
+                     language=ML,
+                      ,keywordstyle=[6]{\itshape}%
+                      ,morekeywords=[6]{args_type}%
+                    }%
+
+\lstnewenvironment{sml}[1][]{\lstset{style=sml,
+    backgroundcolor=\color{Blue!4},
+    frame=lines,
+    basicstyle=\footnotesize\ttfamily,#1}}{}
+%%% 
+\def\inlinesml{\lstinline[style=sml,breaklines=true,mathescape,breakatwhitespace=true]}

examples/scholarly_paper/2022-phd-poster/document/preamble.tex

@@ -0,0 +1,45 @@
+%% This is a placeholder for user-specific configuration and packages. 
+
+\usepackage{stmaryrd}
+\IfFileExists{beramono.sty}{\usepackage[scaled=0.88]{beramono}}{}%
+\IfFileExists{upquote.sty}{\usepackage{upquote}}{}%
+\usepackage{textcomp}
+\usepackage{xcolor}
+\usepackage{paralist}
+\usepackage{listings}
+\usepackage{lstisadof}
+\usepackage{xspace}
+
+\newcommand{\fixIsarList}{\vspace{-\topsep}\vspace{-\baselineskip}\mbox{}\\[0pt]\noindent}
+
+%\nolinenumbers
+\title{<TITLE>}
+\author{<AUTHOR>}
+%\author{First Author\inst{1}\orcidID{0000-1111-2222-3333}}
+%\author{First Author\inst{1}\orcidID{0000-1111-2222-3333} \and
+%Second Author\inst{2,3}\orcidID{1111-2222-3333-4444}}
+%\institute{Inst1}
+%\institute{ Inst1 \and Inst2 \and Inst3}
+%\titlerunning{Proving Ontology-Relations, Testing Ontology Instances}
+%\author{Idir Ait-Sadoune}
+%  {LMF, CentraleSupélec, Université Paris-Saclay, Paris, France}
+%  {idir.aitsadoune@centralesupelec.fr}
+%  {https://orcid.org/0000-0002-6484-8276}
+%  {}
+%\author{Nicolas Méric}
+%  {LMF, Université Paris-Saclay, Paris, France}
+%  {nicolas.meric@universite-paris-saclay.fr}
+%  {https://orcid.org/0000-0002-0756-7072}
+%  {}
+%\author{Burkhart Wolff}
+%  {LMF, Université Paris-Saclay, Paris, France}
+%  {burkhart.wolff@universite-paris-saclay.fr}
+%  {}
+%  {}
+%\Copyright{Idir Ait-Sadoune, Nicolas Méric, and Burkhart Wolff}
+%\authorrunning{I. Ait-Sadoune, N. Méric and B. Wolff}
+%\keywords{Ontologies, Formal Documents, Formal Development, Isabelle/HOL, Ontology Mapping}
+%\ccsdesc{Computing methodologies~Ontology engineering}
+%\ccsdesc{Information systems~Ontologies}
+%\ccsdesc{Theory of computation~Interactive proof systems}
+%\ccsdesc{Theory of computation~Higher order logic}

src/DOF/Isa_DOF.thy

@@ -1010,8 +1010,6 @@ fun elaborate_instances_list thy isa_name _ _ _ =
     val base_name' = DOF_core.get_class_name_without_prefix (base_name_without_suffix)
     val class_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
                                                 (base_name')
-    val class_list_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
-                                                (base_name' ^ " List.list")
     val tab = #tab(#docobj_tab(DOF_core.get_data_global thy))
     val table_list = Symtab.dest tab
     fun get_instances_name_list _ [] = []
@@ -1028,13 +1026,7 @@ fun elaborate_instances_list thy isa_name _ _ _ =
           end
     val long_class_name = DOF_core.read_cid_global thy base_name'
     val values_list = get_instances_name_list long_class_name table_list
-    val hol_list_terms_list =
-      fold
-        (fn x =>
-         fn y =>
-         Const (@{const_name "Cons"}, [class_typ, class_list_typ] ---> class_list_typ) $ x $ y)
-        values_list (Const (@{const_name "Nil"}, class_list_typ))
-  in hol_list_terms_list end
+  in HOLogic.mk_list class_typ values_list end
 
 fun declare_class_instances_annotation thy doc_class_name =
   let

src/document-templates/root-2022-phd-poster.tex

@@ -0,0 +1,610 @@
+\RequirePackage{ifvtex}
+\documentclass[25pt, a0paper, portrait]{tikzposter}
+\usepackage[T1]{fontenc}
+\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage[utf8]{inputenc}
+\usepackage{textcomp}
+\bibliographystyle{abbrvnat}
+\usepackage[english]{babel}
+\RequirePackage[caption]{subfig}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\IfFileExists{DOF-core.sty}{}{%
+  \PackageError{DOF-core}{Isabelle/DOF not installed. 
+    This is a Isabelle_DOF project. The document preparation requires
+    the Isabelle_DOF component from:
+    <isadofurl>
+  }{For further help, see <isadofurl>}
+}
+\input{ontologies}
+\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
+\usepackage{amsmath}
+\usepackage{DOF-amssymb}
+\usepackage[numbers, sort&compress, sectionbib]{natbib}
+\usepackage{graphicx}
+\usepackage{hyperref}
+\setcounter{tocdepth}{3} 
+\hypersetup{%
+   bookmarksdepth=3
+  ,pdfpagelabels
+  ,pageanchor=true
+  ,bookmarksnumbered
+  ,plainpages=false
+} % more detailed digital TOC (aka bookmarks)
+\sloppy
+\allowdisplaybreaks[4]
+\urlstyle{rm}
+\isabellestyle{it}
+
+\newenvironment{frontmatter}{}{}
+
+\title{%
+\parbox{\linewidth}{%
+\centering Isabelle/DOF:\\
+A Framework for Proving Ontology-Relations
+and Runtime Testing Ontology Instances%
+}}
+\author{Idir Ait-Sadoune, Nicolas Méric and Burkhart Wolff}
+\date{\today}
+\institute{Université Paris-Saclay, LMF, France}
+
+\usepackage{blindtext}
+\usepackage{comment}
+\usepackage{amsmath}
+
+% Process bibliography using biber engine.
+%\usepackage[
+  % biber, the default backend of biblatex, supports Ascii,
+  % 8-bit encodings, utf-8, on-the-fly reencoding, locale-specific sorting,
+  % and many other features.
+  % Locale-specific sorting, case-sensitive sorting,
+  % and upper/lowercase precedence are controlled by the options
+  % sortlocale, sortcase, and sortupper, respectively.
+  % See biblatex documentation file biblatex.pdf,
+  % 3.12, 2018/10/30, section 3.1.1, page 45.
+%  backend=biber,
+  % Whether or not to print back references in the bibliography.
+  % The back references are a list of page numbers indicating the pages
+  % on which the respective bibliography entry is cited.
+  % If there are refsection environments in the document,
+  % the back references are local to the reference sections.
+  % Strictly speaking, this option only controls
+  % whether the biblatex package collects the data required
+  % to print such references.
+  % This feature still has to be supported by the selected bibliography style.
+  % All standard styles which come with this package do so.
+  % See biblatex documentation file biblatex.pdf,
+  % 3.12, 2018/10/30, section 3.1.2.1, page 50.
+%  backref=true,
+  % Loads the citation style <file>.cbx.
+  % See § 3.3.1 for an overview of the standard citation styles.
+  % See biblatex documentation file biblatex.pdf,
+  % 3.12, 2018/10/30, section 3.1.1, page 45.
+%  citestyle=alphabetic,
+  % Loads the bibliography style <file>.bbx.
+  % See § 3.3.2 for an overview of the standard bibliography styles.
+  % See biblatex documentation file biblatex.pdf,
+  % 3.12, 2018/10/30, section 3.1.1, page 45.
+%  bibstyle=alphabetic,
+%]{biblatex}
+
+\usetheme{Simple}
+
+% Add bibliography using biblatex macro.
+%
+% Adds a <resource>, such as a .bib file, to the default resource list.
+% This command is only available in the preamble.
+% It replaces the \bibliography legacy command.
+% Note that files must be specified with their full name,
+% including the extension.
+% Do not omit the .bib extension from the filename.
+% Also note that the <resource> is a single resource.
+% If the resources contain duplicate entries (that is, duplicate entrykeys),
+% it is backend dependent what then happens.
+% For example, by default biber will ignore
+% further occurrence of entrykeys unless its --noskipduplicates options is
+% used.
+% Invoke \addbibresource multiple times to add more resources.
+% See biblatex documentation file biblatex.pdf,
+% 3.12, 2018/10/30, section 3.7.1, page 81-82.
+%\addbibresource{bibliography.bib}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\def\HyperFirstAtBeginDocument#1{#1}
+\begin{document}
+\begin{frontmatter}
+  \maketitle
+  % \tableofcontents
+\end{frontmatter}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{columns}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\column{0.33}
+
+% \block{Overview}{
+% \begin{itemize}
+%   \item
+%     Why (Document) Ontologies
+%   \item
+%     Ontologies and Formal Theories
+%   \item
+%     DOF Design
+%   \item
+%     Isabelle/DOF Implementation
+%  \item
+%     Some Application Scenarios
+% \end{itemize}
+% TODO: Add figure
+% PUBLIC RELEASE:
+% http/10.5281/zenodo.3370483
+% }
+
+\block{Linking the Formal and the Informal: Why Ontologies?}{
+% \begin{itemize}
+%   \item
+%     More powerful ITP systems
+%     \(\Longrightarrow\) body of formalised mathematics and engineering
+  % \item
+    The Isabelle Archive Formal of Proof as example :
+\begin{tikzfigure}
+  \includegraphics[width=0.4\linewidth]{%
+    figures/afp_growth_in_number_of_articles.png}
+\end{tikzfigure}
+In 2022, the count stood at 661
+articles, 420 authors and 3.3 M loc !
+  % \item
+}
+Problem of logical consistency technically solved via continuous proof-checking
+
+Problem of knowledge retrieval and of linking semi-formal explanations to
+definitions and proofs still largely open.
+
+The central role in technologies adressing the \emph{knowledge} problem
+is played by \emph{document ontologies}, i.e., a machine-readable form
+of meta-data attached to document-elements as well as their document discourse.
+In order 
+to make these techniques applicable to \emph{formal theory development},
+the following is needed:
+\begin{itemize}
+  \item 
+a general mechanism to define and develop \emph{domain-specific} ontologies,
+\item
+... that should be adapted to entities occurring in formal theories,
+  i.e., provide built-in support for types, terms, theorems, proofs, etc.,
+\item
+ways to annotate meta-data generated by ontologies to the document elements,
+  as ``deep'' as possible, together with strong validation checks,
+\item
+a smooth integration into the theory document development process, and
+\item
+ways to relate ontologies and ontology-conform documents along different
+  ontologies by \emph{ontological mappings} and \emph{data translations}
+  \footnote{We follow throughout this text the terminology established in 
+              \cite{books/daglib/0032976}, pp. 39 ff.}
+\end{itemize}
+    % Rising need for:
+    % % \begin{itemize}
+    %   % \item
+    %     structuring and consistency,
+    %   % \item
+    %     advanced “semantic” search,
+    %   % \item
+    %     tool-interaction.
+   % % \end{itemize}
+% % \end{itemize}
+
+% % \begin{itemize}
+  % % \item
+    % This requires more structured and typed meta-information
+    % % for our application domain
+    % in theory developments
+% % \item
+   % and a better dependency-control of the different document elements,
+   % like
+  % % \begin{itemize}
+    % % \item
+    %   types, terms, theorems
+    % % \item
+    %   code % (proof-terms, proof generating programs, SML, LaTeX etc, but also Scala and C! )
+    % % \item
+    %   text and diagrams %(and perhaps animations, see Jupyter Notebooks https://jupyter.org/ )
+    % % \item
+    %   … and the links between them, requiring notions of
+    %   consistency and coherence for collaborative development
+  % % \end{itemize}
+  % % \item
+
+    % The language in which such meta-information can be specified
+    % is called a \emph{document ontology} %(or \emph{vocabulary})
+% % \end{itemize}
+}
+
+% \block{Linking the Formal and the Informal\\ - Existing Approaches -}{
+% \begin{itemize}
+%   \item
+%     Code Antiquotations as in LISP, MetaML, SML, …
+% \begin{tikzfigure}
+%   \includegraphics[width=0.4\linewidth]{%
+%     figures/code_antiquotations.png}
+% \end{tikzfigure}
+%   \item
+%     Document pragmas as in JavaDoc, Doxygen, et al
+%     TODO: Add figure
+%     \item
+%       Compilation process allows for document generation and some consistency checks
+%       \(\Longrightarrow\) batch mode consistency only.
+%   \item
+%     The Isabelle Approach to “Text-Antiquotations”
+%     (heavily used to assure \emph{coherence} and
+%     \emph{traceability} in the technical documentations and papers)
+%   \item
+%     Definitions and proofs can be mixed with text elements
+%     \begin{tikzfigure}
+%       \includegraphics[width=0.4\linewidth]{%
+%         figures/text_element.png}
+%     \end{tikzfigure}
+%   \item
+%     Text Elements may contain Antiquotations to Formal Content
+%     in the Logical Context, which are checked and animated in the IDE:
+%     \begin{tikzfigure}
+%       \includegraphics[width=0.4\linewidth]{%
+%         figures/text_element_with_formal_content.png}
+%     \end{tikzfigure}
+%   \item
+%     The global doc-generation process yields a presentation in, e.g.,  .pdf :
+%     \begin{tikzfigure}
+%       \includegraphics[width=0.4\linewidth]{%
+%         figures/output.png}
+%     \end{tikzfigure}
+%   \item
+%     Similarly, Isabelle Code uses heavily “SML-Antiquotations” 
+%   \item
+%     SML System Code can be mixed with antiquotations producing
+%     SML level representation of types and terms:
+%     \begin{tikzfigure}
+%       \includegraphics[width=0.4\linewidth]{%
+%         figures/sml_code_with_antiquotations.png}
+%     \end{tikzfigure}
+% \end{itemize}
+% }
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% \column{0.33}
+
+% \block{Isabelle's Document-Centric View on Formal Development}{
+% \begin{itemize}
+%   \item
+%     Primary document type: “XXX.thy”
+%     \begin{tikzfigure}
+%       \includegraphics[width=0.4\linewidth]{%
+%         figures/theories_hierarchy.png}
+%     \end{tikzfigure}
+%   \begin{itemize}
+%     \item
+%       Acyclic Graph of units that consist of
+%       a sequence of \emph{document elements}
+%       called “commands”
+%     \item
+%       commands user-programmable in SML
+%     \item
+%       Support of Cascade Syntax:
+%       @{SML ‹ … @{type ‹  ….  ›} … ›}
+%     \item
+%       Commands are semantically transformers
+%       of the logical context : \(\Theta \Rightarrow \Theta\)
+%     \item
+%       anti-quotations are “semantic macros” and as such partial) functions:
+%       \(\Theta \Rightarrow \text{text}\)
+%       \(\Theta \Rightarrow \text{sml}\)
+%       \(\Theta \Rightarrow \text{term}\)
+%     \item
+%       pervasive continuous build/check of Isabelle/PIDE supports anti-quotations.
+%   \end{itemize}
+% \end{itemize}
+% }
+
+\block{Isabelle/DOF}{
+\begin{itemize}
+  \item
+    DOF : The Document Ontology Framework
+    has been designed as an Isabelle component that attempts to answer these needs.
+  \item
+    Prior Versions of Isabelle/DOF support semantic annotations of text and code-contexts:
+
+    \(
+text*[label::classid, attr1 =E1 , ... attrn =En ]⟨ some semi-formal text ⟩
+\)
+
+\(
+ML*[label::classid, attr1 =E1 , ... attrn =En ] ⟨ some SML code ⟩
+\)
+    TODO: Add figure
+  \item
+    Novelty in Isabelle/DOF: support of \(\lambda\)-term-contexts, e.g.:
+    \(value*[label::classid, attr1 =E1 , ... attrn =En ]⟨ some annotated \lambda-term ⟩\)
+    TODO: Add figure
+
+  formal, machine-checked invariants on meta-data, which correspond to the concept of
+  ``rules'' in OWL~ \cite{OWL2014} or ``constraints'' in UML, and which can be specified in
+  common Isabelle/HOL \(\lambda\)-term syntax.
+\end{itemize}
+
+% \innerblock{Isabelle/DOF}{
+%   AAAAAAAAAAAAAAAAAAAAAAAAAAAAA
+% }
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\column{0.33}
+
+\block{Isabelle/DOF Core : ODL}{
+\begin{itemize}
+  \item
+    The Ontology Definition Language (ODL):
+    The Mechanism to \emph{define} Ontologies
+  \item
+    Features:
+    \begin{tikzfigure}
+      \includegraphics[width=0.4\linewidth]{%
+        figures/odl.png}
+    \end{tikzfigure}
+    \begin{itemize}
+      \item
+        classes (for the “concepts”)
+      \item
+        classes may have attributes
+        with HOL type
+      \item
+        class declarations  can be
+        interleaved with arbitrary HOL
+        declarations
+      \item
+        attributes of class-instances
+        are mutable;  (default) values
+        can be denoted by HOL-terms
+      \item
+        class declarations induce a HOL-type;
+        this allows to establish “ontological links”
+    \end{itemize}
+    \begin{tikzfigure}
+      \includegraphics[width=0.4\linewidth]{%
+        figures/dof_classes.png}
+    \end{tikzfigure}
+    \begin{itemize}
+      \item
+        classes have single inheritance
+        (is a - relation)
+      \item
+        attribute overriding of attributes is possible
+      \item
+        meta-level types of the ITP were included as abstract HOL types;
+        their inhabitance is checked
+        in the global context \(\theta\)
+    \end{itemize}
+\end{itemize}
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% \column{0.33}
+
+\block{DOF Example Document}{
+\begin{itemize}
+  \item
+    Defining the Ontological Context
+\begin{tikzfigure}
+  \includegraphics[width=0.4\linewidth]{%
+    figures/ontological_context.png}
+\end{tikzfigure}
+  \item
+    And there we go:
+    \begin{tikzfigure}
+      \includegraphics[width=0.4\linewidth]{%
+        figures/dof_document.png}
+    \end{tikzfigure}
+  \item
+    … where title* and
+    abstract* are macros
+    for text*[a::title,…],
+    etc…
+  \item
+    … and the meta-data
+    instances are a, abs,
+    intro, T1, attached to
+    these  doc elements  …
+\end{itemize}
+}
+
+\block{Isabelle/DOF Core : Class Invariants}{
+\begin{itemize}
+  \item
+    ODL used already  \(\lambda\)-(ground)-terms to denote values for attributes.
+  \item
+    New: ODL uses arbitrary \(\lambda\)-terms containing generated
+    \emph{term-antiquotations in invariants},
+    attribute definitions and commands like value*
+  \item
+    Eg.: Invariants for
+    \begin{tikzfigure}
+      \includegraphics[width=0.4\linewidth]{%
+        figures/classes_with_invariant.png}
+    \end{tikzfigure}
+    TODO: FIGURE MUST BU UPDATED!!! See original example
+    \begin{itemize}
+      \item
+        data-integrity constraints
+      \item
+        … using “built-in” term antiquotations for “term”, “typ”, “thm”
+      \item
+        may use DOF-generated term-antiquotations
+        like @{result ‘’<some result instance>’’}
+        or @{introduction ‘’intro’’} or @{instance-of ‘’result’’}, etc.
+      \item
+        “a result text element must provide evidence
+        in form of a proven theorem …”
+    \end{itemize}
+\end{itemize}
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\column{0.33}
+
+\block{Consequences}{
+\begin{itemize}
+  \item
+    If an ODL ontology generates “intra-logical” representations,
+    what’s the benefit ?
+    \begin{itemize}
+      \item
+        We don't have to learn a new (meta)-language
+      \item
+        We can define new operations on them inside
+        the  logic and develop their theory …
+      \item
+        … to develop a query language, for example:
+        \(
+          value*⟨ filter (is_interesting) @\{instances-of "result"\} ⟩
+        \)
+      \item
+        We can relate ontologies and ontology instances
+        by formal proof (‘’ontology alignment, ontology mapping’’)
+    \end{itemize}
+\end{itemize}
+}
+
+\block{Consequences: Example Proof of an Ontology Mapping}{
+\begin{itemize}
+  \item
+    A “‘Generic’ Reference Ontology” vs. a “‘local’ Ontology”
+    \begin{tikzfigure}
+      \includegraphics[width=0.4\linewidth]{%
+        figures/reference_ontology.png}
+    \end{tikzfigure}
+    \begin{tikzfigure}
+      \includegraphics[width=0.4\linewidth]{%
+        figures/local_ontology.png}
+    \end{tikzfigure}
+    \begin{tikzfigure}
+      \includegraphics[width=0.4\linewidth]{%
+        figures/morphism.png}
+    \end{tikzfigure}
+  \item
+    “The mapping is correct (preserves the invariants)”
+    \begin{tikzfigure}
+      \includegraphics[width=0.4\linewidth]{%
+        figures/invariant_preserved.png}
+    \end{tikzfigure}
+\end{itemize}
+}
+
+\block{But what “are” ontology-generated term antiquotations  ???}{
+\begin{itemize}
+  \item
+    First of all: how are they processed:
+    \begin{itemize}
+      \item parsing
+      \item type checking
+      \item validation (an argument is indeed a valid reference in the context)
+      \item expansion (replacement of a reference against logical terms)
+      \item evaluation (to SML code, or by nbe)
+    \end{itemize}
+  \item
+    Then “built-in” term-anti quotations can be:
+    \begin{itemize}
+      \item
+        just uninterpreted constants (without expansion)
+        TODO: Add figure
+      \item
+        a ‘’shallow’’ data-type representation (without expansion)
+        TODO: Add figure
+      \item
+        or a “deep” data-type representation into an Isabelle
+        Meta-Model such as [Nipkow,Rosskopf 21] (with expansion)
+        TODO: Add figure
+    \end{itemize}
+\end{itemize}
+}
+
+\block{Conclusion}{
+\begin{itemize}
+  \item
+    DOF provides a framework
+    \begin{itemize}
+      \item
+        for defining ontologies in the context of ITP systems
+      \item
+        its typed ! It has a logical interpretation !
+      \item
+        provides a generated infrastructure for meta-data of
+        types, terms, thm’s and text and code elements
+    \end{itemize}
+  \item
+    DOF provides a framework to enforce on-the-fly
+    ontology-conform documentation checking
+  \item
+    DOF provides infrastructure for proofs over the
+    logical representation of ontologies and meta-data …
+  \item
+    Ontologies generating meta-data can be used
+    for other forms of Tool Interaction via “deep
+    interpretations” into a meta-model
+  \item
+    (P)IDE's are more than just a technical asset
+  \item
+    … it is a corner-stone for a revolution
+    \begin{itemize}
+      \item
+        1970’ies          TEXT
+      \item
+        1990’ies          HYPERTEXT
+      \item
+        2010’ies          REACTIVE DOCUMENTS
+      \item
+        2020’ies          SEMANTIC DOCUMENTS (???)
+    \end{itemize}
+\end{itemize}
+}
+
+\end{columns}
+
+\input{session}
+
+\block{References}{
+% optional bibliography
+\IfFileExists{root.bib}{{\bibliography{root}}}{}
+\end{document}
+%\printbibliography
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% \begin{columns}
+%     \column{0.4}
+%     \block{More text}{Text and more text}
+    
+%     \column{0.6}
+%     \block{Something else}{Here, \blindtext \vspace{4cm}}
+%     \note[
+%         targetoffsetx=-9cm, 
+%         targetoffsety=-6.5cm, 
+%         width=0.5\linewidth
+%         ]
+%         {e-mail \texttt{welcome@overleaf.com}}
+% \end{columns}
+
+% \begin{columns}
+%     \column{0.5}
+%     \block{A figure}
+%     {
+%         \begin{tikzfigure}
+%             % \includegraphics[width=0.4\textwidth]{images/overleaf-logo}
+%         \end{tikzfigure}
+%     }
+%     \column{0.5}
+%     \block{Description of the figure}{\blindtext}
+% \end{columns}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\end{document}
+

src/document-templates/root-eptcs-UNSUPPORTED.tex

@@ -1,5 +1,5 @@
-%% Copyright (c) 2019 University of Exeter
-%%               2018-2019 University of Paris-Saclay
+%% Copyright (c) 2019-2022 University of Exeter
+%%               2018-2022 University of Paris-Saclay
 %%               2018-2019 The University of Sheffield
 %%
 %% License:

src/document-templates/root-lipics-v2021.tex

@@ -10,8 +10,9 @@
 %%   OR
 %%   The 2-clause BSD-style license.
 %%
+%%   SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
 
-%%   2022/01/25 Unreleased/Isabelle2021
+%%   <isadofltxversion>
 
 %% Warning: Do Not Edit!
 %% =====================
@@ -81,10 +82,7 @@
 \maketitle
 \input{session}
 % optional bibliography
-\IfFileExists{root.bib}{%
-{\small  
-  \bibliography{root}
-}}{}
+\IfFileExists{root.bib}{{\small\bibliography{root}}}{}
 \end{document}
 
 %%% Local Variables:

src/document-templates/root-lncs.tex

@@ -1,5 +1,5 @@
-%% Copyright (c) 2019 University of Exeter
-%%               2018-2019 University of Paris-Saclay
+%% Copyright (c) 2019-2022 University of Exeter
+%%               2018-2022 University of Paris-Saclay
 %%               2018-2019 The University of Sheffield
 %%
 %% License:
@@ -26,6 +26,7 @@
 \usepackage[T1]{fontenc}
 \usepackage[utf8]{inputenc}
 \usepackage[USenglish]{babel}
+\bibliographystyle{splncs04}
 \usepackage{isabelle}
 \usepackage{xcolor}
 \usepackage{isabellesym}
@@ -68,17 +69,6 @@
 \renewcommand{\floatpagefraction}{0.7}        % require fuller float pages
 \renewcommand{\dblfloatpagefraction}{0.7}     % require fuller float pages
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%% Overrides the (rightfully issued) warning by Koma Script that \rm
-%%% etc. should not be used (they are deprecated since more than a
-%%% decade)
-  \DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
-  \DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
-  \DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
-  \DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
-  \DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
 \begin{document}
 \selectlanguage{USenglish}%
 \renewcommand{\bibname}{References}%
@@ -97,14 +87,7 @@
 \maketitle
 \input{session}
 % optional bibliography
-\IfFileExists{root.bib}{%
-{\small   \renewcommand{\doi}[1]{}
-  \newcommand{\urlprefix}{}
-
-  \bibliographystyle{splncs04}
-  
-  \bibliography{root}
-}}{}
+\IfFileExists{root.bib}{{\small\bibliography{root}}}{}
 \end{document}
 
 %%% Local Variables:

src/document-templates/root-scrartcl.tex

@@ -1,5 +1,5 @@
-%% Copyright (c) 2019 University of Exeter
-%%               2018-2019 University of Paris-Saclay
+%% Copyright (c) 2019-2022 University of Exeter
+%%               2018-2022 University of Paris-Saclay
 %%               2018-2019 The University of Sheffield
 %%
 %% License:
@@ -57,16 +57,7 @@
 \allowdisplaybreaks[4]
 \urlstyle{rm}
 \isabellestyle{it}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%% Overrides the (rightfully issued) warning by Koma Script that \rm
-%%% etc. should not be used (they are deprecated since more than a
-%%% decade)
-  \DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
-  \DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
-  \DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
-  \DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
-  \DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \newenvironment{frontmatter}{}{}
 
 \begin{document}
@@ -76,9 +67,7 @@
 \end{frontmatter}
 \input{session}
 % optional bibliography
-\IfFileExists{root.bib}{%
-    \bibliography{root}
-}{}
+\IfFileExists{root.bib}{{\bibliography{root}}}{}
 \end{document}
 
 %%% Local Variables:

src/document-templates/root-scrreprt-modern.tex

@@ -1,5 +1,5 @@
-%% Copyright (c) 2019 University of Exeter
-%%               2018-2019 University of Paris-Saclay
+%% Copyright (c) 2019-2022 University of Exeter
+%%               2018-2022 University of Paris-Saclay
 %%               2018-2019 The University of Sheffield
 %%
 %% License:
@@ -78,16 +78,7 @@
 \allowdisplaybreaks[4]
 \urlstyle{sf}
 \isabellestyle{it}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%% Overrides the (rightfully issued) warning by Koma Script that \rm
-%%% etc. should not be used (they are deprecated since more than a
-%%% decade)
-  \DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
-  \DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
-  \DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
-  \DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
-  \DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \newenvironment{frontmatter}{}{}
 
 \begin{document}
@@ -103,9 +94,7 @@
 \end{frontmatter}
 \input{session}
 % optional bibliography
-\IfFileExists{root.bib}{%
-    \bibliography{root}
-}{}
+\IfFileExists{root.bib}{{\bibliography{root}}}{}
 \end{document}
 
 %%% Local Variables:

src/document-templates/root-scrreprt.tex

@@ -1,5 +1,5 @@
-%% Copyright (c) 2019 University of Exeter
-%%               2018-2019 University of Paris-Saclay
+%% Copyright (c) 2019-2022 University of Exeter
+%%               2018-2022 University of Paris-Saclay
 %%               2018-2019 The University of Sheffield
 %%
 %% License:
@@ -57,16 +57,7 @@
 \allowdisplaybreaks[4]
 \urlstyle{rm}
 \isabellestyle{it}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%% Overrides the (rightfully issued) warning by Koma Script that \rm
-%%% etc. should not be used (they are deprecated since more than a
-%%% decade)
-  \DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
-  \DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
-  \DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
-  \DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
-  \DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \newenvironment{frontmatter}{}{}
 
 \begin{document}
@@ -82,9 +73,7 @@
 \end{frontmatter}
 \input{session}
 % optional bibliography
-\IfFileExists{root.bib}{%
-    \bibliography{root}
-}{}
+\IfFileExists{root.bib}{{\bibliography{root}}}{}
 \end{document}
 
 %%% Local Variables:

src/document-templates/root-svjour3-UNSUPPORTED.tex

@@ -1,5 +1,5 @@
-%% Copyright (c) 2019-2021 University of Exeter
-%%               2018-2021 University of Paris-Saclay
+%% Copyright (c) 2019-2022 University of Exeter
+%%               2018-2022 University of Paris-Saclay
 %%               2018-2019 The University of Sheffield
 %%
 %% License:
@@ -12,7 +12,7 @@
 %%
 %%   SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
 
-%%   2021/03/22 Unreleased/Isabelle2021
+%%   <isadofltxversion>
 
 %% Warning: Do Not Edit!
 %% =====================
@@ -61,17 +61,6 @@
 \usepackage[caption]{subfig}
 \usepackage[size=footnotesize]{caption}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%% Overrides the (rightfully issued) warning by Koma Script that \rm
-%%% etc. should not be used (they are deprecated since more than a
-%%% decade)
-  \DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
-  \DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
-  \DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
-  \DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
-  \DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
 \begin{document}
 \selectlanguage{USenglish}%
 \renewcommand{\bibname}{References}%
@@ -85,16 +74,10 @@
 \newcommand{\subfigureautorefname}{\figureautorefname}
 \newcommand{\lstnumberautorefname}{Line}
 
-
-
 \maketitle
 \input{session}
 % optional bibliography
-\IfFileExists{root.bib}{%
-{\small  
-  \newcommand{\urlprefix}{}
-  \bibliography{root}
-}}{}
+\IfFileExists{root.bib}{{\bibliography{root}}}{}
 \end{document}
 
 %%% Local Variables:

src/ontologies/CC_v3.1_R5/CC_terminology.thy

@@ -3,7 +3,7 @@ chapter\<open>Common Criteria Definitions\<close>
 (*<<*)
 theory CC_terminology
 
-imports  "../technical_report/technical_report" 
+imports  "Isabelle_DOF.technical_report" 
 
 begin
 
@@ -427,4 +427,4 @@ Definition*[evalu_def, tag="'' Evaluator''"]
  as mandatory statement of evaluation criteria when determining the assurance 
  of @{docitem toe_def}s and when evaluating @{docitem pp_def}s and @{docitem st_def}s.\<close>
 
-end
+end

src/ontologies/CC_v3.1_R5/CC_v3_1_R5.thy

@@ -15,7 +15,7 @@
 
 (*<*)
 theory  "CC_v3_1_R5"
-  imports  "../technical_report/technical_report" 
+  imports  "Isabelle_DOF.technical_report" 
            "CC_terminology"
 
 

src/ontologies/CENELEC_50128/CENELEC_50128.thy

@@ -25,7 +25,7 @@ identifies:
 
 (*<<*)  
 theory CENELEC_50128
-  imports  "../technical_report/technical_report"
+  imports  "Isabelle_DOF.technical_report"
 begin
 
 (* this is a hack and should go into an own ontology, providing thingsd like:
@@ -771,4 +771,4 @@ ML
   Syntax.read_typ                  @{context} "hypothesis"  handle  _ => dummyT;
   Proof_Context.init_global; \<close>
 
-end
+end

src/ontologies/Conceptual/Conceptual.thy

@@ -13,8 +13,11 @@
 
 section\<open>A conceptual introduction into DOF and its features:\<close>
 
-theory Conceptual
-  imports "../../DOF/Isa_DOF" "../../DOF/Isa_COL"
+theory 
+  Conceptual
+imports 
+  "Isabelle_DOF.Isa_DOF" 
+  "Isabelle_DOF.Isa_COL"
 begin
 
 

src/ontologies/scholarly_paper/DOF-scholarly_paper.sty

@@ -60,9 +60,15 @@
                 \newcommand{\inst}[1]{}%
             }%
             {%
+              \@ifclassloaded{tikzposter}%
+              {%
+                 \newcommand{\inst}[1]{}%
+              }%
+              {%
               \PackageError{DOF-scholarly_paper}
                           {Scholarly Paper only supports LNCS or scrartcl as document class.}
                           {}\stop%
+              }%
             }%
           }%
         }%

src/ontologies/scholarly_paper/scholarly_paper.thy

@@ -14,7 +14,7 @@
 section\<open>An example ontology for scientific, MINT-oriented papers.\<close>
 
 theory scholarly_paper
-  imports "../../DOF/Isa_COL"
+  imports "Isabelle_DOF.Isa_COL"
   keywords "author*" "abstract*"
            "Definition*" "Lemma*" "Theorem*"  :: document_body
 

src/ontologies/small_math/small_math.thy

@@ -14,7 +14,7 @@
 section\<open>An example ontology for a math paper\<close>
 
 theory small_math
-   imports "../../DOF/Isa_COL"
+   imports "Isabelle_DOF.Isa_COL"
 begin
 
 doc_class title =

src/ontologies/technical_report/technical_report.thy

@@ -14,7 +14,7 @@
 section\<open>An example ontology for a scholarly paper\<close>
 
 theory technical_report
-   imports "../scholarly_paper/scholarly_paper"
+   imports "Isabelle_DOF.scholarly_paper"
 begin              
 
 (* for reports paper: invariant: level \<ge> -1 *)

src/tests/Evaluation.thy

@@ -200,7 +200,10 @@ text\<open>Assertions must be true, hence the error:\<close>
 assert*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>*)
 
 term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
-assert*\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
+assert*[assertionA::A]\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
+
+text-macro*[assertionAA::A]\<open>@{A [display] "assertionA"}\<close> 
+text\<open>... and here we reference @{A [display] \<open>assertionA\<close>}.\<close>
 
 assert*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>