exceptional storage of submission version

The author_finite invariant did not check anything,
as the the elements of the set are already type checked.
The new author_set definition checks that the set is not empty, i.e.,
that myintro has an author.

README.md

@@ -43,6 +43,7 @@ The final step for the installation is:
 foo@bar:~$ isabelle build -D .
 ```
 
+
 This will compile Isabelle/DOF and run the example suite.
 
 ## Usage

examples/CENELEC_50128/mini_odo/ROOT

@@ -12,3 +12,4 @@ session "mini_odo" = "Isabelle_DOF" +
     "figures/odometer.jpeg"
     "figures/three-phase-odo.pdf"
     "figures/wheel-df.png"
+    "figures/CENELEC-Fig.3-docStructure.png"

examples/scholarly_paper/2020-iFM-CSP/paper.thy

@@ -3,7 +3,6 @@ theory "paper"
   imports "Isabelle_DOF.scholarly_paper"
 begin
 
-
 open_monitor*[this::article]
 
 declare[[ strict_monitor_checking  = false]]
@@ -48,8 +47,8 @@ abstract*[abs, keywordlist="[\<open>Shallow Embedding\<close>,\<open>Process-Alg
 
    If you consider citing this paper, please refer to @{cite "HOL-CSP-iFM2020"}.
 \<close>
-text\<open>\<close>
-section*[introheader::introduction,main_author="Some(@{docitem ''bu''}::author)"]\<open> Introduction \<close> 
+
+section*[introheader::introduction,main_author="Some(@{docitem ''bu''}::author)"]\<open> Introduction \<close>
 text*[introtext::introduction]\<open>
 Communicating Sequential Processes (\<^csp>) is a language 
 to specify and verify patterns of interaction of concurrent systems.

examples/scholarly_paper/2021-ITP-PMTI/ROOT

@@ -0,0 +1,24 @@
+session "2021-ITP-PMTI" = "Isabelle_DOF" +
+  options [document = pdf, document_output = "output", document_build = dof]
+  theories
+    "paper"
+  document_files
+    "isadof.cfg"
+    "root.bib"
+    "preamble.tex"
+    "figures/Req-Appl-ex.png"
+    "figures/formal-development.png"
+    "figures/Req-Def-ex.png"
+    "figures/odometer.jpeg"
+    "figures/cicm2018-combined.png"
+    "figures/three-phase-odo.pdf"
+    "figures/df-numerics-encshaft.png"
+    "figures/wheel-df.png"
+    "figures/invariant-checking-violated-example.png"
+    "figures/inherited-invariant-checking-violated-example.png"
+    "figures/term-context-checking-example.png"
+    "figures/term-context-failed-checking-example.png"
+    "figures/term-context-evaluation-example.png"
+    "figures/term-context-failed-evaluation-example.png"
+    "figures/term-context-equality-evaluation-example.png"
+    "lstisadof.sty"

examples/scholarly_paper/2021-ITP-PMTI/archiv/latex_compilation_material/DOF-COL.sty

@@ -0,0 +1,99 @@
+%% 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
+
+\NeedsTeXFormat{LaTeX2e}\relax
+\ProvidesPackage{DOF-COL}
+  [<isadofltxversion>%
+  Document-Type Support Framework for Isabelle.]
+
+\RequirePackage{DOF-core}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: figure*
+\NewEnviron{isamarkupfigure*}[1][]{\isaDof[env={figure},#1]{\BODY}}
+\newisadof{figure.Isa_COL.figure}%
+[label=,type=%
+,Isa_COL.figure.relative_width=%
+,Isa_COL.figure.placement=%
+,Isa_COL.figure.src=%
+,Isa_COL.figure.spawn_columns=enum False True%
+][1]{%
+  \begin{figure}[]
+    \centering
+    \ifcommandkey{Isa_COL.figure.relative_width}
+    {%
+      \gdef\dof@width{\commandkey{Isa_COL.figure.relative_width}}
+      \gdef\dof@src{\commandkey{Isa_COL.figure.src}}
+      \FPdiv\scale{\dof@width}{100}%
+      \includegraphics[width=\scale\textwidth]{\dof@src}%
+    }{%
+      \gdef\dof@src{\commandkey{Isa_COL.figure.src}}
+      \includegraphics[]{\dof@src}%
+    } 
+    \caption{#1}\label{\commandkey{label}}%
+  \end{figure}
+}
+% end: figure*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: side_by_side_figure*
+\NewEnviron{isamarkupsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure*}[1][]{\isaDof[env={side_by_side_figure},#1]{\BODY}}
+\newisadof{side_by_side_figure.Isa_COL.side_by_side_figure}%
+[label=,type=%
+,Isa_COL.figure.relative_width=%
+,Isa_COL.figure.placement=%
+,Isa_COL.figure.src=%
+,Isa_COL.side_by_side_figure.anchor=%
+,Isa_COL.side_by_side_figure.caption=%
+,Isa_COL.side_by_side_figure.relative_width2=%
+,Isa_COL.side_by_side_figure.src2=%
+,Isa_COL.side_by_side_figure.anchor2=%
+,Isa_COL.side_by_side_figure.caption2=%
+,Isa_COL.side_by_side_figure.placement=%
+,Isa_COL.figure.spawn_columns=enum False True%
+][1]{%
+  \begin{figure}[]
+    \subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor}}\commandkey{Isa_COL.side_by_side_figure.caption}]%
+      {\ifcommandkey{Isa_COL.figure.relative_width}%
+       {%
+          \gdef\dof@width{\commandkey{Isa_COL.figure.relative_width}}
+          \gdef\dof@src{\commandkey{Isa_COL.figure.src}}
+          \FPdiv\scale{\dof@width}{100}%
+          \includegraphics[width=\scale\textwidth]{\dof@src}%
+        }{%
+          \gdef\dof@src{\commandkey{Isa_COL.figure.src}}
+          \includegraphics[]{\dof@src}%
+        }% 
+      }%
+      \hfill%
+      \subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor2}}\commandkey{Isa_COL.side_by_side_figure.caption2}]%
+      {\ifcommandkey{Isa_COL.side_by_side_figure.relative_width2}%
+        {%
+          \gdef\dof@width{\commandkey{Isa_COL.side_by_side_figure.relative_width2}}
+          \gdef\dof@src{\commandkey{Isa_COL.side_by_side_figure.src2}}
+          \FPdiv\scale{\dof@width}{100}%
+          \includegraphics[width=\scale\textwidth]{\dof@src}%
+        }{%
+          \gdef\dof@src{\commandkey{Isa_COL.side_by_side_figure.src2}}
+          \includegraphics[]{\dof@src}%
+        }% 
+      }%
+    \caption{#1}\label{\commandkey{label}}%
+  \end{figure}
+}
+% end: side_by_side_figure*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

examples/scholarly_paper/2021-ITP-PMTI/archiv/latex_compilation_material/DOF-amssymb.sty

@@ -0,0 +1,26 @@
+%% Copyright (C) 2021 University of Exeter
+%%               2021 University of Paris-Saclay
+%%
+%% 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
+
+
+\NeedsTeXFormat{LaTeX2e}\relax
+\ProvidesPackage{DOF-amssymb}
+  [<isadofltxversion>%
+  Document-Type Support Framework for Isabelle (amssymb wrapper for lualatex/pdflatex).]
+
+\usepackage{ifxetex,ifluatex}
+\ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex
+  \usepackage{amssymb}
+\else % if luatex or xetex
+  \usepackage{unicode-math}
+  \usepackage{latexsym}
+\fi

examples/scholarly_paper/2021-ITP-PMTI/archiv/latex_compilation_material/DOF-core.sty

@@ -0,0 +1,160 @@
+%% 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
+
+\NeedsTeXFormat{LaTeX2e}\relax
+\ProvidesPackage{DOF-core}
+  [<isadofltxversion>%
+  Document-Type Support Framework for Isabelle.]
+
+\RequirePackage{keycommand}
+\RequirePackage{environ}
+\RequirePackage{graphicx}
+\RequirePackage{xspace}
+\RequirePackage{etoolbox}
+\RequirePackage{fp}
+
+\newcommand{\isabelleurl}{UNDEFINED}
+\newcommand{\dofurl}{UNDEFINED}
+\newcommand{\dof@isabelleversion}{UNDEFINED}
+\newcommand{\isabellefullversion}{UNDEFINED\xspace}
+\newcommand{\dof@version}{UNDEFINED}
+\newcommand{\dof@artifacturl}{UNDEFINED}
+\newcommand{\doflatestversion}{UNDEFINED}
+\newcommand{\isadoflatestdoi}{UNDEFINED}
+\newcommand{\isadofgenericdoi}{UNDEFINED}
+\newcommand{\isabellelatestversion}{Isabelle2019}
+
+%%% CONFIG %%%
+
+\newcommand{\isabelleversion}{\dof@isabelleversion\xspace}
+\newcommand{\dofversion}{\dof@version\xspace}
+\newcommand{\isadofversion}{\dofversion/\isabelleversion}
+\newcommand{\isadoflatestversion}{\doflatestversion/\isabellelatestversion}
+\newcommand{\isadofdir}{Isabelle_DOF-\dof@version_\dof@isabelleversion}
+\newcommand{\isadofdirn}{Isabelle\_DOF-\dof@version\_\dof@isabelleversion}
+\newcommand{\isadofarchive}{\isadofdir.tar.xz}
+\newcommand{\isadofarchiven}{\isadofdirn.tar.xz}
+\newcommand{\isadofarchiveurl}{\dof@artifacturl/\isadofarchive}
+
+\newcommand{\isadof}{Isabelle/DOF\xspace}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: newcommand wrapper
+\newcommand\newisadof[1]{\expandafter\newkeycommand\csname isaDof.#1\endcsname}%
+\newcommand\renewisadof[1]{\expandafter\renewkeycommand\csname isaDof.#1\endcsname}%
+\newcommand\provideisadof[1]{\expandafter\providekeycommand\csname isaDof.#1\endcsname}%
+% end: newcommand wrapper
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: generic dispatcher
+\newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,type={dummyT},args={}][1]{%
+  \ifcsname isaDof.\commandkey{type}\endcsname%
+      \csname isaDof.\commandkey{type}\endcsname%
+              [label=\commandkey{label},\commandkey{args}]{#1}%
+  \else\relax\fi%
+  \ifcsname isaDof.\commandkey{env}.\commandkey{type}\endcsname%
+      \csname isaDof.\commandkey{env}.\commandkey{type}\endcsname%
+              [label=\commandkey{label},\commandkey{args}]{#1}%
+  \else%
+      \message{Isabelle/DOF: Using default LaTeX representation for concept %
+        "\commandkey{env}.\commandkey{type}".}%
+      \ifcsname isaDof.\commandkey{env}\endcsname%
+         \csname isaDof.\commandkey{env}\endcsname%
+                [label=\commandkey{label}]{#1}%
+      \else%
+      \errmessage{Isabelle/DOF: No LaTeX representation for concept %
+        "\commandkey{env}.\commandkey{type}" defined and no default %
+        definition for "\commandkey{env}" available either.}%
+      \fi%
+  \fi%
+}
+% end: generic dispatcher
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: text*-dispatcher
+\NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}}
+% end: text*-dispatcher
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: chapter*-dispatcher
+\NewEnviron{isamarkupchapter*}[1][]{\isaDof[env={chapter},#1]{\BODY}}
+% end: chapter*-dispatcher
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: section*-dispatcher
+\NewEnviron{isamarkupsection*}[1][]{\isaDof[env={section},#1]{\BODY}}
+% end: section*-dispatcher
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: subsection*-dispatcher
+\NewEnviron{isamarkupsubsection*}[1][]{\isaDof[env={subsection},#1]{\BODY}}
+% end: subsection*-dispatcher
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: subsubsection*-dispatcher
+\NewEnviron{isamarkupsubsubsection*}[1][]{\isaDof[env={subsubsection},#1]{\BODY}}
+% end: subsubsection*-dispatcher
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: paragraph*-dispatcher
+\NewEnviron{isamarkupparagraph*}[1][]{\isaDof[env={paragraph},#1]{\BODY}}
+% end: paragraph*-dispatcher
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: text default implementation
+\newisadof{text}[label=,type=][1]{%
+  \begin{isamarkuptext}\label{\commandkey{label}}%
+    #1
+  \end{isamarkuptext}%
+}
+% end: text default implementation
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: chapter/section default implementations
+\newisadof{chapter}[label=,type=][1]{%
+  \isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue%
+}
+\newisadof{section}[label=,type=][1]{%
+  \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
+}
+\newisadof{subsection}[label=,type=][1]{%
+  \isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
+}
+\newisadof{subsubsection}[label=,type=][1]{%
+  \isamarkupfalse\isamarkupsubsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
+}
+\newisadof{paragraph}[label=,type=][1]{%
+  \isamarkupfalse\isamarkupparagraph{#1}\label{\commandkey{label}}\isamarkuptrue%
+}
+% end: chapter/section default implementations
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: label and ref
+\newisadof{label}[label=,type=][1]{\label{#1}}
+\newisadof{ref}[label=,type=][1]{\autoref{#1}}
+\newisadof{macroDef}[label=,type=][1]{MMM \label{#1}}        %% place_holder
+\newisadof{macroExp}[label=,type=][1]{MMM \autoref{#1}}   %% place_holder
+% end: label and ref
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

examples/scholarly_paper/2021-ITP-PMTI/archiv/latex_compilation_material/DOF-scholarly_paper.sty

@@ -0,0 +1,499 @@
+%% 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
+
+\NeedsTeXFormat{LaTeX2e}\relax
+\ProvidesPackage{DOF-scholarly_paper}
+  [2021/03/22 Unreleased/Isabelle2021%
+  Document-Type Support Framework for Isabelle (LNCS).]
+
+\RequirePackage{DOF-COL}
+\RequirePackage{ifthen}
+
+\RequirePackage{ifthen}
+\newboolean{DOF@scholarlypaper@force}
+\DeclareOption{force}{\setboolean{DOF@scholarlypaper@force}{true}}
+
+\ProcessOptions\relax
+
+\ifthenelse{\boolean{DOF@scholarlypaper@force}}{%
+}{%
+\@ifclassloaded{llncs}%
+  {}%
+  {%
+    \@ifclassloaded{scrartcl}%
+    {%
+      \newcommand{\institute}[1]{}%
+      \newcommand{\inst}[1]{}%
+      \newcommand{\orcidID}[1]{}%
+      \newcommand{\email}[1]{}%
+      \RequirePackage{DOF-scholarly_paper-thm}%
+    }%
+    {%
+      \@ifclassloaded{lipics-v2021}%
+      {%
+        \newcommand{\institute}[1]{}%
+        \newcommand{\inst}[1]{}%
+        \newcommand{\orcidID}[1]{}%
+        \newcommand{\email}[1]{}%
+      }%
+      {%
+        {%
+          \@ifclassloaded{eptcs}%
+          {%
+            \newcommand{\inst}[1]{}%
+            \newcommand{\orcidID}[1]{}%
+          }%
+          {%
+            \@ifclassloaded{svjour3}%
+            {%
+                \newcommand{\inst}[1]{}%
+            }%
+            {%
+              \PackageError{DOF-scholarly_paper}
+                          {Scholarly Paper only supports LNCS or scrartcl as document class.}
+                          {}\stop%
+            }%
+          }%
+        }%
+      }%
+    }
+  }
+}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: title*
+\NewEnviron{isamarkuptitle*}[1][]{\isaDof[env={title},#1]{\BODY}}
+\newisadof{title.scholarly_paper.title}%
+[label=,type=%
+,scholarly_paper.title.short_title=%
+][1]{%
+  \immediate\write\@auxout{\noexpand\title{#1}}%
+}
+% end: title*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: subtitle*
+\NewEnviron{isamarkupsubtitle*}[1][]{\isaDof[env={subtitle},#1]{\BODY}}
+\newisadof{subtitle.scholarly_paper.subtitle}%
+[label=,type=%
+,scholarly_paper.subtitle.abbrev=%
+][1]{%
+  \immediate\write\@auxout{\noexpand\subtitle{#1}}%
+}
+% end: subtitle*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: scholarly_paper.author
+\def\dof@author{}%
+\def\dof@affiliation{}%
+
+\newcommand{\DOFauthor}{\author{\dof@author}}
+\newcommand{\DOFinstitute}{\institute{\dof@affiliation}}
+
+\AtBeginDocument{%
+  \DOFauthor
+  \DOFinstitute
+}
+
+\def\leftadd#1#2{\expandafter\leftaddaux\expandafter{#1}{#2}{#1}}
+\def\leftaddaux#1#2#3{\gdef#3{#1#2}}
+
+\newcounter{dof@cnt@author}
+\newcommand{\addauthor}[1]{%
+  \ifthenelse{\equal{\dof@author}{}}{%
+    \gdef\dof@author{#1}%
+  }{%
+    \leftadd\dof@author{\protect\and #1}%
+  }
+}
+
+\newcommand{\addaffiliation}[1]{%
+  \ifthenelse{\equal{\dof@affiliation}{}}{%
+    \gdef\dof@affiliation{#1}%
+  }{%
+    \leftadd\dof@affiliation{\protect\and #1}%
+  }
+}
+
+\NewEnviron{isamarkupauthor*}[1][]{\isaDof[env={text},#1]{\BODY}}
+\provideisadof{text.scholarly_paper.author}%
+[label=,type=%
+,scholarly_paper.author.email=%
+,scholarly_paper.author.affiliation=%
+,scholarly_paper.author.orcid=%
+,scholarly_paper.author.http_site=%
+][1]{%
+  \stepcounter{dof@cnt@author}
+  \def\dof@a{\commandkey{scholarly_paper.author.affiliation}}
+  \ifthenelse{\equal{\commandkey{scholarly_paper.author.orcid}}{}}{%
+    \protected@write\@auxout{}{\string\addauthor{#1\string\inst{\thedof@cnt@author}}}%
+  }{%
+    \protected@write\@auxout{}{\string\addauthor{#1\string\inst{\thedof@cnt@author}\string\orcidID{\commandkey{scholarly_paper.author.orcid}}}}%
+  }
+  \protected@write\@auxout{}{\string\addaffiliation{\dof@a\\\string\email{\commandkey{scholarly_paper.author.email}}}}%
+}
+% end: scholarly_paper.author
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: scholarly_paper.abstract
+\providecommand{\keywords}[1]{\mbox{}\\[2ex]\mbox{}\noindent{\textbf{Keywords:}} #1}
+\NewEnviron{isamarkupabstract*}[1][]{\isaDof[env={text.scholarly_paper.abstract},#1]{\BODY}}
+\newisadof{text.scholarly_paper.abstract}%
+[label=,type=%
+,scholarly_paper.abstract.keywordlist=%
+][1]{%
+  \begin{isamarkuptext}%
+    \begin{abstract}%
+      #1%
+      \ifthenelse{\equal{\commandkey{scholarly_paper.abstract.keywordlist}}{}}{}{%     
+        \keywords{\commandkey{scholarly_paper.abstract.keywordlist}}%
+      }%
+    \end{abstract}%
+  \end{isamarkuptext}%
+}
+
+\newtheorem{axiom}{Axiom}
+\newtheorem{ruleX}{Rule} % apparent name-clash with s th from libraries...
+\newtheorem{assertion}{Assertion} 
+
+% \newcommand{\formalMathStmt[label, mcc, ]
+% end: scholarly_paper.abstract
+% | "rule" | "assn" | "expl" | rem      | "notation" | "terminology"
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newisadof{text.scholarly_paper.math_content}%
+[label=,type=%
+ , scholarly_paper.math_content.short_name ={} % {} or \relax
+ , scholarly_paper.math_content.mcc     = % "def" | "axm" | "thm" | "lem" | "prop" | "rule" | "assn"
+ , Isa_COL.text_element.level         =%
+ , Isa_COL.text_element.referentiable =%
+ , Isa_COL.text_element.variants      =%
+ , scholarly_paper.text_section.main_author  =%
+ , scholarly_paper.text_section.fixme_list   =%
+ , Isa_COL.text_element.level                =%
+ , scholarly_paper.technical.definition_list =%
+ , scholarly_paper.technical.status          =%
+ ]
+ [1]
+ {%
+    \begin{isamarkuptext}%
+        \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{defn}}
+                   {%
+                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+                         {\begin{definition} \label{\commandkey{label}} #1 \end{definition} }
+                         {\begin{definition} [\commandkey{scholarly_paper.math_content.short_name}] 
+                                             \label{\commandkey{label}} #1 
+                          \end{definition}}
+                    }%
+                   }%
+        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{axm}}    
+                   {%
+                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+                         {\begin{axiom} \label{\commandkey{label}} #1 \end{axiom} }
+                         {\begin{axiom} [\commandkey{scholarly_paper.math_content.short_name}] 
+                                        \label{\commandkey{label}} #1 
+                          \end{axiom}}
+                    }%
+                   }%
+        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{thm}}    
+                   {%
+                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+                         {\begin{theorem} \label{\commandkey{label}} #1 \end{theorem} }
+                         {\begin{theorem} [\commandkey{scholarly_paper.math_content.short_name}] 
+                                          \label{\commandkey{label}} #1 
+                          \end{theorem}}
+                    }%
+                   }%
+        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{lem}}    
+                   {%
+                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+                         {\begin{lemma} \label{\commandkey{label}} #1 \end{lemma} }
+                         {\begin{lemma} [\commandkey{scholarly_paper.math_content.short_name}] 
+                                        \label{\commandkey{label}} #1 
+                          \end{lemma}}
+                    }%
+                   }%
+        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{expl}}    
+                   {%
+                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+                         {\begin{example} \label{\commandkey{label}} #1 \end{example} }
+                         {\begin{example} [\commandkey{scholarly_paper.math_content.short_name}] 
+                                          \label{\commandkey{label}} #1 
+                          \end{example}}
+                    }%
+                   }%
+        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{cor}}    
+                   {%
+                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+                         {\begin{corrollary} \label{\commandkey{label}} #1 \end{corrollary} }
+                         {\begin{corrollary} [\commandkey{scholarly_paper.math_content.short_name}] 
+                                             \label{\commandkey{label}} #1 
+                          \end{corrollary}}
+                    }%
+                   }%
+        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{prop}}    
+                   {%
+                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+                         {\begin{property} \label{\commandkey{label}} #1 \end{property} }
+                         {\begin{property} [\commandkey{scholarly_paper.math_content.short_name}] 
+                                           \label{\commandkey{label}} #1 
+                          \end{property}}
+                    }%
+                   }%
+        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{rule}}    
+                   {%
+                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+                         {\begin{ruleX} \label{\commandkey{label}} #1 \end{ruleX} }
+                         {\begin{ruleX} [\commandkey{scholarly_paper.math_content.short_name}] 
+                                        \label{\commandkey{label}} #1 
+                          \end{ruleX}}
+                    }%
+                   }%
+        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{rem}}    
+                   {%
+                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+                         {\begin{remark}  \label{\commandkey{label}} #1 \end{remark} }
+                         {\begin{remark} [\commandkey{scholarly_paper.math_content.short_name}] 
+                                          \label{\commandkey{label}} #1 
+                          \end{remark}}
+                    }%
+                   }%
+        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{assn}}    
+                   {%
+                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+                         {\begin{assertion} \label{\commandkey{label}} #1 \end{assertion} }
+                         {\begin{assertion} [\commandkey{scholarly_paper.math_content.short_name}] 
+                                             \label{\commandkey{label}} #1 
+                          \end{assertion}}
+                    }%
+                   }%
+        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{notation}}    
+                   {%
+                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+                         {\begin{notation} \label{\commandkey{label}} #1 \end{notation} }
+                         {\begin{notation} [\commandkey{scholarly_paper.math_content.short_name}] 
+                                           \label{\commandkey{label}} #1 
+                          \end{notation}}
+                    }%
+                   }%
+        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{terminology}}    
+                   {%
+                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+                         {\begin{terminology} \label{\commandkey{label}} #1 \end{terminology} }
+                         {\begin{terminology} [\commandkey{scholarly_paper.math_content.short_name}] 
+                                              \label{\commandkey{label}} #1 
+                          \end{terminology}}
+                    }%
+                   }%
+        {%     
+           \typeout{Internal error: enumeration out of sync with ontology scholarly-paper.} 
+        }%
+        }%
+        }%
+        }%
+        }%
+        }%
+        }%
+        }%
+        }%
+        }%
+        }%
+        }%      
+    \end{isamarkuptext}%
+ } 
+
+
+
+% end: scholarly_paper.math_content
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Besser: Einfach durchreichen wg Vererbung !
+\newisadof{text.scholarly_paper.math_example}%
+[label=,type=%
+ , scholarly_paper.math_content.short_name =%
+ , scholarly_paper.math_content.mcc =%
+ , Isa_COL.text_element.level         =%
+ , Isa_COL.text_element.referentiable =%
+ , Isa_COL.text_element.variants      =%
+ , scholarly_paper.text_section.main_author  =%
+ , scholarly_paper.text_section.fixme_list   =%
+ , scholarly_paper.technical.definition_list =%
+ , scholarly_paper.technical.status          =%
+ ]
+ [1]
+ {%
+    \begin{isamarkuptext}%
+        \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{expl}}{
+              \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+                         {\begin{example} \label{\commandkey{label}} #1 \end{example} }
+                         {\begin{example} [\commandkey{scholarly_paper.math_content.short_name}]
+                                          \label{\commandkey{label}} #1  
+                          \end{example}}
+          }{%     
+          #1%
+        }%
+    \end{isamarkuptext}%
+ }
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\NewEnviron{isamarkupDefinition*}[1][]{\isaDof[env={text},#1]{\BODY}}
+\newisadof{text.scholarly_paper.definition}%
+[label=,type=%
+ , scholarly_paper.math_content.short_name =%
+ , scholarly_paper.math_content.mcc =%
+ , Isa_COL.text_element.level         =%
+ , Isa_COL.text_element.referentiable =%
+ , Isa_COL.text_element.variants      =%
+ , scholarly_paper.text_section.main_author  =%
+ , scholarly_paper.text_section.fixme_list   =%
+ , Isa_COL.text_element.level                =%
+ , scholarly_paper.technical.definition_list =%
+ , scholarly_paper.technical.status          =%
+ ]
+ [1]
+ {%
+    \begin{isamarkuptext}%
+        \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{defn}}{
+              \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+                         {\begin{definition} \label{\commandkey{label}} #1 \end{definition} }
+                         {\begin{definition} [\commandkey{scholarly_paper.math_content.short_name}] \label{\commandkey{label}} #1 \end{definition}}
+          }{%     
+          #1%
+        }%
+    \end{isamarkuptext}%
+ }
+
+% An experiment in inheritance of the default behaviour.
+% \newisadof{text.scholarly_paper.definition}%
+% [label=,type=%
+%  , scholarly_paper.math_content.short_name =%
+%  , scholarly_paper.math_content.mcc =%
+%  , Isa_COL.text_element.level         =%
+%  , Isa_COL.text_element.referentiable =%
+%  , Isa_COL.text_element.variants      =%
+%  , scholarly_paper.text_section.main_author  =%
+%  , scholarly_paper.text_section.fixme_list   =%
+%  , scholarly_paper.technical.definition_list =%
+%  , scholarly_paper.technical.status          =%
+%  ]
+%  [1]
+%  {%
+%     \cscommand{text.scholarly_paper.math_content}%
+%     [label=\commandkey{label},type=\commandkey{type}%
+%     , scholarly_paper.math_content.short_name   =\commandkey{scholarly_paper.math_content.short_name}%
+%     , scholarly_paper.math_content.mcc          =\commandkey{scholarly_paper.math_content.mcc}%
+%     , Isa_COL.text_element.level                =\commandkey{Isa_COL.text_element.level}%
+%     , Isa_COL.text_element.referentiable        =\commandkey{Isa_COL.text_element.referentiable}%
+%     , Isa_COL.text_element.variants             =\commandkey{Isa_COL.text_element.variants}%
+%     , scholarly_paper.text_section.main_author  =\commandkey{scholarly_paper.text_section.main_author}%
+%     , scholarly_paper.text_section.fixme_list   =\commandkey{scholarly_paper.text_section.fixme_list}%
+%     , scholarly_paper.technical.definition_list =\commandkey{scholarly_paper.technical.definition_list}%
+%     , scholarly_paper.technical.status          =\commandkey{scholarly_paper.technical.status}%
+%     ]
+%     {#1}%
+%  }
+ 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% Besser: Einfach durchreichen wg Vererbung !
+\NewEnviron{isamarkupLemma*}[1][]{\isaDof[env={text.scholarly_paper.lemma},#1]{\BODY}}
+\newisadof{text.scholarly_paper.lemma}%
+[label=,type=%
+ , scholarly_paper.math_content.short_name =%
+ , scholarly_paper.math_content.mcc =%
+ , Isa_COL.text_element.level         =%
+ , Isa_COL.text_element.referentiable =%
+ , Isa_COL.text_element.variants      =%
+ , scholarly_paper.text_section.main_author  =%
+ , scholarly_paper.text_section.fixme_list   =%
+ , Isa_COL.text_element.level                =%
+ , scholarly_paper.technical.definition_list =%
+ , scholarly_paper.technical.status          =%
+ ]
+ [1]
+ {%
+    \begin{isamarkuptext}%
+        \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{lem}}{
+              \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+                         {\begin{lemma} \label{\commandkey{label}} #1 \end{lemma} }
+                         {\begin{lemma} [\commandkey{scholarly_paper.math_content.short_name}] \label{\commandkey{label}} #1 \end{lemma}}
+          }{%     
+          #1%
+        }%
+    \end{isamarkuptext}%
+ } 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Besser: Einfach durchreichen wg Vererbung !
+\NewEnviron{isamarkupTheorem*}[1][]{\isaDof[env={text.scholarly_paper.theorem},#1]{\BODY}}
+\newisadof{text.scholarly_paper.theorem}%
+[label=,type=%
+ , scholarly_paper.math_content.short_name =%
+ , scholarly_paper.math_content.mcc =%
+ , Isa_COL.text_element.level         =%
+ , Isa_COL.text_element.referentiable =%
+ , Isa_COL.text_element.variants      =%
+ , scholarly_paper.text_section.main_author  =%
+ , scholarly_paper.text_section.fixme_list   =%
+ , Isa_COL.text_element.level                =%
+ , scholarly_paper.technical.definition_list =%
+ , scholarly_paper.technical.status          =%
+ ]
+ [1]
+ {%
+    \begin{isamarkuptext}%
+        \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{thm}}{
+              \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+                         {\begin{theorem} \label{\commandkey{label}} #1 \end{theorem} }
+                         {\begin{theorem} [\commandkey{scholarly_paper.math_content.short_name}] \label{\commandkey{label}} #1 \end{theorem}}
+          }{%     
+          #1%
+        }%
+    \end{isamarkuptext}%
+ } 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Generic Example. Different inheritance hierachy.
+\newisadof{text.scholarly_paper.example}%
+[label=,type=%
+ , Isa_COL.text_element.level         =%
+ , Isa_COL.text_element.referentiable =%
+ , Isa_COL.text_element.variants      =%
+ , scholarly_paper.text_section.main_author  =%
+ , scholarly_paper.text_section.fixme_list   =%
+ , scholarly_paper.technical.definition_list =%
+ , scholarly_paper.example.status     =%
+ , scholarly_paper.example.short_name =%
+ ]
+ [1]
+ {%
+    \begin{isamarkuptext}%
+        \ifthenelse{\equal{\commandkey{scholarly_paper.example.status}}{semiformal}}{
+              \ifthenelse{\equal{\commandkey{scholarly_paper.example.short_name}} {} }  
+                         {\begin{example} \label{\commandkey{label}} #1 \end{example} }
+                         {\begin{example} [\commandkey{scholarly_paper.example.short_name}] %
+                                          \label{\commandkey{label}} #1 %
+                          \end{example}} %
+                         }%
+        {%     
+          #1%
+        }%
+    \end{isamarkuptext}%
+ }
+
+
+%% Miscellaneous
+\usepackage{xspace}
+\newcommand{\ie}{i.\,e.\xspace}
+\newcommand{\eg}{e.\,g.\xspace}
+\newcommand{\etc}{etc}
+

examples/scholarly_paper/2021-ITP-PMTI/archiv/latex_compilation_material/ontologies.tex

@@ -0,0 +1,2 @@
+\usepackage{DOF-core}
+\usepackage{DOF-scholarly_paper}

examples/scholarly_paper/2021-ITP-PMTI/archiv/latex_compilation_material/root.bbl

@@ -0,0 +1,146 @@
+\begin{thebibliography}{10}
+\providecommand{\url}[1]{\texttt{#1}}
+\providecommand{\urlprefix}{URL }
+\providecommand{\doi}[1]{https://doi.org/#1}
+
+\bibitem{AehligHN12}
+Aehlig, K., Haftmann, F., Nipkow, T.: A compiled implementation of
+  normalisation by evaluation. J. Funct. Program.  \textbf{22}(1),  9--30
+  (2012). \doi{10.1017/S0956796812000019}
+
+\bibitem{BGPP95}
+Ameur, Y.A., Besnard, F., Girard, P., Pierra, G., Potier, J.: Formal
+  specification and metaprogramming in the {EXPRESS} language. In: SEKE'95, Proceedings. pp.
+  181--188. Knowledge Systems Institute (1995)
+
+\bibitem{10.1007/978-3-540-76298-0_52}
+Auer, S., Bizer, C., Kobilarov, G., Lehmann, J., Cyganiak, R., Ives, Z.:
+  {DB}pedia: A nucleus for a web of open data. In: The Semantic Web.
+  pp. 722--735. Springer, Berlin, Heidelberg (2007)
+
+\bibitem{brucker.ea:isabelle-ontologies:2018}
+Brucker, A.D., Ait-Sadoune, I., Crisafulli, P., Wolff, B.: Using the {Isabelle}
+  ontology framework: Linking the formal with the informal.
+  In: CICM. No. 11006 in LNCS, Springer-Verlag, Heidelberg (2018).
+  \doi{10.1007/978-3-319-96812-4_3}
+
+\bibitem{brucker.ea:upf-firewall:2017}
+Brucker, A.D., Br{\"u}gger, L., Wolff, B.: Formal network models and their
+  application to firewall policies. AFP (Jan 2017),
+  \url{http://www.isa-afp.org/entries/UPF_Firewall.shtml}
+
+\bibitem{brucker.ea:afp-core-dom:2018}
+Brucker, A.D., Herzberg, M.: The {Core} {DOM}. AFP (Dec
+  2018),
+  \url{http://www.isa-afp.org/entries/Core_DOM.html}
+
+\bibitem{brucker.ea:featherweight:2014}
+Brucker, A.D., Tuong, F., Wolff, B.: {Featherweight} {OCL}: A proposal for a
+  machine-checked formal semantics for {OCL} 2.5. AFP (Jan 2014),
+  \url{http://www.isa-afp.org/entries/Featherweight_OCL.shtml}
+
+\bibitem{brucker.ea:isabelledof:2019}
+Brucker, A.D., Wolff, B.: {Isabelle/DOF}: Design and implementation. In:
+  SEFM. No. 11724 in LNCS,
+  Springer-Verlag, Heidelberg (2019). \doi{10.1007/978-3-030-30446-1_15}
+
+\bibitem{DBLP:conf-ifm-BruckerW19}
+Brucker, A.D., Wolff, B.: Using ontologies in formal developments targeting
+  certification. In: {IFM} 2019, Proceedings. LNCS, vol. 11918, pp.
+  65--82. Springer (2019). \doi{10.1007/978-3-030-34968-4_4}
+
+\bibitem{bsi:50128:2014}
+Bs en 50128:2011: Railway applications -- communication, signalling and
+  processing systems -- software for railway control and protecting systems.
+  Standard, Britisch Standards Institute (BSI) (Apr 2014)
+
+\bibitem{books/daglib/0032976}
+Euzenat, J., Shvaiko, P.: Ontology Matching, Second Edition. Springer (2013).
+  \doi{10.1007/978-3-642-38721-0}
+
+\bibitem{atl}
+{Eclipse Foundation}: Atl - a model transformation technology,
+  \url{https://www.eclipse.org/atl/}, {A}ccessed: 2022-03-15
+
+\bibitem{FotsoFLM18}
+Fotso, S.J.T., Frappier, M., Laleau, R., Mammar, A.: Modeling the hybrid
+  {ERTMS/ETCS} level 3 standard using a formal requirements engineering
+  approach. In: Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 6th
+  International Conference, {ABZ}, Southampton, UK. LLNCS, vol. 10817, pp.
+  262--276. Springer (2018). \doi{10.1007/978-3-319-91271-4_18}
+
+\bibitem{HaftmannN10}
+Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In:
+  {FLOPS} 2010, Proceedings. LNCS, vol.~6009, pp. 103--117.
+  Springer (2010). \doi{10.1007/978-3-642-12251-4_9}
+
+\bibitem{SPARCv8-AFP}
+Hou, Z., Sanan, D., Tiu, A., Liu, Y.: A formal model for the sparcv8 isa and a
+  proof of non-interference for the leon3 processor. AFP
+  (Oct 2016), \url{http://isa-afp.org/entries/SPARCv8.html}
+
+\bibitem{CakeML-AFP}
+Hupel, L., Zhang, Y.: Cakeml. AFP (Mar 2018),
+  \url{http://isa-afp.org/entries/CakeML.html}
+
+\bibitem{klein.ea:comprehensive:2014}
+Klein, G., Andronick, J., Elphinstone, K., Murray, T.C., Sewell, T., Kolanski,
+  R., Heiser, G.: Comprehensive formal verification of an {OS} microkernel.
+  {ACM} Trans. Comput. Syst.  \textbf{32}(1),  2:1--2:70 (2014).
+  \doi{10.1145/2560537}
+
+\bibitem{KohlhaseR21}
+Kohlhase, M., Rabe, F.: Experiences from exporting major proof assistant
+  libraries. J. Autom. Reason.  \textbf{65}(8),  1265--1298 (2021).
+  \doi{10.1007/s10817-021-09604-0}
+
+\bibitem{AFP-ref22}
+{M.Eberl and G. Klein and A. Lochbihler and T. Nipkow and L. Paulson and R.
+  Thiemann (eds)}: Archive of Formal Proofs. \url{https://afp-isa.org}
+  (2022), {A}ccessed: 2022-03-15
+
+\bibitem{MendilASMP21}
+Mendil, I., A{\"{\i}}t-Ameur, Y., Singh, N.K., M{\'{e}}ry, D., Palanque, P.A.:
+  Standard conformance-by-construction with event-b. In: {FMICS}.
+  LNCS, vol. 12863, pp. 126--146. Springer (2021).
+  \doi{10.1007/978-3-030-85248-1_8}
+
+\bibitem{protege}
+Musen, M.A.: The prot\'{e}g\'{e} project: A look back and a look forward. AI
+  Matters  \textbf{1}(4),  4–12 (jun 2015). \doi{10.1145/2757001.2757003}
+
+\bibitem{Nevzorova2014OntoMathPO}
+Nevzorova, O., Zhiltsov, N., Kirillovich, A., Lipachev, E.K.:
+  Onto{Ma}th\textsuperscript{PRO} ontology: {A} linked data hub for
+  mathematics. ArXiv  \textbf{abs/1407.4833} (2014).
+  \doi{10.1007/978-3-319-11716-4_9}
+
+\bibitem{Splay_Tree-AFP}
+Nipkow, T.: Splay tree. AFP (Aug 2014),
+  \url{http://isa-afp.org/entries/Splay_Tree.html}
+
+\bibitem{10.1007/978-3-030-79876-5_6}
+Nipkow, T., Ro{\ss}kopf, S.: Isabelle's metalogic: Formalization and proof
+  checker. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction -- CADE
+  28. pp. 93--110. Springer International Publishing, Cham (2021)
+
+\bibitem{OWL2014}
+Sengupta, K., Hitzler, P.: Web ontology language {(OWL)}. In: Encyclopedia of
+  Social Network Analysis and Mining, pp. 2374--2378 (2014).
+  \doi{10.1007/978-1-4614-6170-8_113}
+
+\bibitem{Security_Protocol_Refinement-AFP}
+Sprenger, C., Somaini, I.: Developing security protocols by refinement. AFP (May 2017),
+  \url{http://isa-afp.org/entries/Security_Protocol_Refinement.html}
+
+\bibitem{verbeek.ea:formal:2014}
+Verbeek, F., Tverdyshev, S., Havle, O., Blasum, H., Langenstein, B., Stephan,
+  W., Nemouchi, Y., Feliachi, A., Wolff, B., Schmaltz, J.: Formal specification
+  of a generic separation kernel. AFP (Jul 2014),
+  \url{http://isa-afp.org/entries/CISC-Kernel.html}
+
+\bibitem{wenzel:isabelle-isar:2020}
+Wenzel, M.: The Isabelle/Isar Reference Manual (2020), part of the Isabelle
+  distribution.
+
+\end{thebibliography}

examples/scholarly_paper/2021-ITP-PMTI/archiv/latex_compilation_material/root.tex

@@ -0,0 +1,113 @@
+%% Copyright (c) 2019 University of Exeter
+%%               2018-2019 University of Paris-Saclay
+%%               2018-2019 The University of Sheffield
+%%
+%% 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
+
+%%   <isadofltxversion>
+
+%% Warning: Do Not Edit!
+%% =====================
+%% This is the root file for the Isabelle/DOF using the lncs class.
+%%
+%% All customization and/or additional packages should be added to the file
+%% preamble.tex.
+
+\RequirePackage{ifvtex}
+\documentclass{llncs}
+\usepackage[T1]{fontenc}
+\usepackage[utf8]{inputenc}
+\usepackage[USenglish]{babel}
+\usepackage{isabelle}
+\usepackage{xcolor}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{DOF-amssymb}
+\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{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}
+\usepackage[caption]{subfig}
+\usepackage[size=footnotesize]{caption}
+
+\renewcommand{\topfraction}{0.9}      % max fraction of floats at top
+\renewcommand{\bottomfraction}{0.8}   % max fraction of floats at bottom
+\setcounter{topnumber}{2}
+\setcounter{bottomnumber}{2}
+\setcounter{totalnumber}{4}     % 2 may work better
+\setcounter{dbltopnumber}{2}    % for 2-column pages
+\renewcommand{\dbltopfraction}{0.9}   % fit big float above 2-col. text
+\renewcommand{\textfraction}{0.07}    % allow minimal text w. figs
+\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}%
+\renewcommand{\figurename}{Fig.}
+\renewcommand{\abstractname}{Abstract.}
+\renewcommand{\subsubsectionautorefname}{Sect.}
+\renewcommand{\subsectionautorefname}{Sect.}
+\renewcommand{\sectionautorefname}{Sect.}
+\renewcommand{\figureautorefname}{Fig.}
+\newcommand{\subtableautorefname}{\tableautorefname}
+\newcommand{\subfigureautorefname}{\figureautorefname}
+\newcommand{\lstnumberautorefname}{Line}
+
+
+
+\maketitle
+\input{session}
+% optional bibliography
+\IfFileExists{root.bib}{%
+{\small  
+  \newcommand{\urlprefix}{}
+
+  \bibliographystyle{splncs04}
+  
+  \bibliography{root}
+}}{}
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:

examples/scholarly_paper/2021-ITP-PMTI/document/isadof.cfg

@@ -0,0 +1,2 @@
+Template: lncs
+Ontology: scholarly_paper

examples/scholarly_paper/2021-ITP-PMTI/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/2021-ITP-PMTI/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}

examples/scholarly_paper/2021-ITP-PMTI/output/document/build

@@ -0,0 +1,160 @@
+#!/usr/bin/env bash
+# Copyright (c) 2019 University of Exeter
+#               2018-2019 University of Paris-Saclay
+#               2018-2019 The University of Sheffield
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions
+# are met:
+# 1. Redistributions of source code must retain the above copyright
+#    notice, this list of conditions and the following disclaimer.
+# 2. Redistributions in binary form must reproduce the above copyright
+#    notice, this list of conditions and the following disclaimer in
+#    the documentation and/or other materials provided with the
+#    distribution.
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
+# FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
+# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
+# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
+# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+# ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+# POSSIBILITY OF SUCH DAMAGE.
+#
+# SPDX-License-Identifier: BSD-2-Clause
+
+set -e
+OUTFORMAT=${1:-pdf}
+NAME=${2:-root}
+
+ROOT_NAME="root_$NAME"
+
+install_dof_tex(){
+    cp $ISABELLE_DOF_HOME/src/document-templates/* .
+    cp $ISABELLE_DOF_HOME/src/DOF/*/*.sty .
+    cp $ISABELLE_DOF_HOME/src/ontologies/*/*.sty . 
+    
+    ISABELLE_SHORT_VERSION=`echo $ISABELLE_VERSION | sed -e 's/:.*$//'`
+    sed -i -e "s|%%% CONFIG %%%| \
+      \\\\renewcommand{\\\\dof@isabelleversion}{$ISABELLE_SHORT_VERSION} \
+      \\\\renewcommand{\\\\isabellelatestversion}{$DOF_LATEST_ISABELLE} \
+      \\\\renewcommand{\\\\isabellefullversion}{$ISABELLE_VERSION\\\\xspace} \
+      \\\\renewcommand{\\\\dof@version}{$DOF_VERSION} \
+      \\\\renewcommand{\\\\doflatestversion}{$DOF_LATEST_VERSION} \
+      \\\\renewcommand{\\\\isadoflatestdoi}{$DOF_LATEST_DOI} \
+      \\\\renewcommand{\\\\isadofgenericdoi}{$DOF_GENERIC_DOI} \
+      \\\\renewcommand{\\\\isabelleurl}{$ISABELLE_URL} \
+      \\\\renewcommand{\\\\dofurl}{$DOF_URL} \
+      \\\\renewcommand{\\\\dof@artifacturl}{https://$DOF_ARTIFACT_HOST/$DOF_ARTIFACT_DIR}|" \
+      "DOF-core.sty"
+
+    
+    sed -i -e "s|<isadofurl>|$DOF_URL|" *.sty
+    sed -i -e "s|<isadofurl>|$DOF_URL|" *.tex
+    LTX_VERSION="$DOF_DATE $DOF_VERSION/$ISABELLE_SHORT_VERSION"
+    sed -i -e "s|<isadofltxversion>|$LTX_VERSION|" *.tex
+    sed -i -e "s|<isadofltxversion>|$LTX_VERSION|" *.sty
+}
+
+[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root"
+
+if [ -f "$DIR/$ROOT_NAME.tex" ]; then 
+    >&2 echo ""
+    >&2 echo "Error: Found root file ($DIR/$ROOT_NAME.tex)"
+    >&2 echo "====="
+    >&2 echo "Isabelle/DOF does not use the Isabelle root file setup. Please check"
+    >&2 echo "your project setup. Your $DIR/isadof.cfg should define a Isabelle/DOF"
+    >&2 echo "template and your project should not include a root file."
+    >&2 echo ""
+    exit 1
+fi
+
+if [ ! -f isadof.cfg ]; then 
+    >&2 echo ""
+    >&2 echo "Error: Isabelle/DOF document setup not correct"
+    >&2 echo "====="
+    >&2 echo "Could not find isadof.cfg. Please upgrade your Isabelle/DOF document"
+    >&2 echo "setup manually."
+    exit 1
+fi
+
+TEMPLATE=""
+ONTOLOGY="core"
+CONFIG="isadof.cfg"
+while IFS= read -r line;do
+    fields=($(printf "%s" "$line"|cut -d':' -f1- | tr ':' ' '))
+    if [[ "${fields[0]}" = "Template" ]]; then 
+	TEMPLATE="${fields[1]}"
+    fi                      
+    if [[ "${fields[0]}" = "Ontology" ]]; then 
+	ONTOLOGY="$ONTOLOGY ${fields[1]}"
+    fi
+done < $CONFIG
+
+for o in $ONTOLOGY; do
+  >&2 echo "\usepackage{DOF-$o}" >> ontologies.tex;
+done
+
+install_dof_tex
+
+ROOT="root-$TEMPLATE.tex"
+if [ ! -f $ROOT ]; then 
+    >&2 echo ""
+    >&2 echo "Error: Isabelle/DOF document setup not correct"
+    >&2 echo "====="
+    >&2 echo "Could not find root file ($ROOT)."
+    >&2 echo "Please upgrade your Isabelle/DOF document setup manually."
+    exit 1
+fi
+
+cp $ROOT root.tex
+
+# delete outdated aux files from previous runs
+rm -f *.aux 
+
+sed -i -e 's/<@>/@/g' *.tex 
+
+$ISABELLE_PDFLATEX root && \
+{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_BIBTEX root; } && \
+{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_MAKEINDEX root; } && \
+$ISABELLE_PDFLATEX root && \
+$ISABELLE_PDFLATEX root
+
+MISSING_CITATIONS=`grep 'Warning.*Citation' root.log | awk '{print $5}' | sort  -u`
+if [ "$MISSING_CITATIONS" != "" ]; then
+    >&2 echo ""
+    >&2 echo "ERROR (Isabelle/DOF): document referencing inconsistent due to missing citations: "
+    >&2 echo "$MISSING_CITATIONS"
+    exit 1
+fi
+DANGLING_REFS=`grep 'Warning.*Refer' root.log | awk '{print $4}' | sort  -u`
+if [ "$DANGLING_REFS" != "" ]; then
+    >&2 echo ""
+    >&2 echo "ERROR (Isabelle/DOF): document referencing inconsistent due to dangling references:"
+    >&2 echo "$DANGLING_REFS"
+    >&2 echo ""
+    exit 1
+fi
+if [ -f "root.blg" ]; then 
+    >&2 echo "BibTeX Warnings:"
+    >&2 echo "================"
+    >&2 grep Warning  root.blg | sed -e 's/Warning--//'
+    >&2 echo ""
+fi
+>&2 echo "Layout Glitches:"
+>&2 echo "================"
+>&2 echo -n "Number of overfull hboxes: "
+>&2 grep 'Overfull .hbox' root.log | wc -l
+>&2 echo -n "Number of underfull hboxes: "
+>&2 grep 'Underfull .hbox' root.log | wc -l
+>&2 echo -n "Number of overfull vboxes: "
+grep 'Overfull .vbox' root.log | wc -l
+>&2 echo -n "Number of underfull vboxes: "
+grep 'Underfull .vbox' root.log | wc -l
+>&2 echo ""
+
+exit 0

examples/scholarly_paper/2021-ITP-PMTI/output/document/comment.sty

@@ -0,0 +1,278 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Comment.sty   version 3.6, October 1999
+%
+% Purpose:
+% selectively in/exclude pieces of text: the user can define new
+% comment versions, and each is controlled separately.
+% Special comments can be defined where the user specifies the
+% action that is to be taken with each comment line.
+%
+% Author
+%    Victor Eijkhout
+%    Department of Computer Science
+%    University of Tennessee
+%    107 Ayres Hall
+%    Knoxville TN 37996
+%    USA
+%
+%    victor@eijkhout.net
+%
+% This program is free software; you can redistribute it and/or
+% modify it under the terms of the GNU General Public License
+% as published by the Free Software Foundation; either version 2
+% of the License, or (at your option) any later version.
+% 
+% This program is distributed in the hope that it will be useful,
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+% GNU General Public License for more details.
+%
+% For a copy of the GNU General Public License, write to the 
+% Free Software Foundation, Inc.,
+% 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA,
+% or find it on the net, for instance at
+% http://www.gnu.org/copyleft/gpl.html
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% This style can be used with plain TeX or LaTeX, and probably
+% most other packages too.
+%
+% Usage: all text included between
+%    \comment ... \endcomment
+% or \begin{comment} ... \end{comment}
+% is discarded. 
+%
+% The opening and closing commands should appear on a line
+% of their own. No starting spaces, nothing after it.
+% This environment should work with arbitrary amounts
+% of comment, and the comment can be arbitrary text.
+%
+% Other `comment' environments are defined by
+% and are selected/deselected with
+% \includecomment{versiona}
+% \excludecoment{versionb}
+%
+% These environments are used as
+% \versiona ... \endversiona
+% or \begin{versiona} ... \end{versiona}
+% with the opening and closing commands again on a line of 
+% their own.
+%
+% LaTeX users note: for an included comment, the
+% \begin and \end lines act as if they don't exist.
+% In particular, they don't imply grouping, so assignments 
+% &c are not local.
+%
+% Special comments are defined as
+% \specialcomment{name}{before commands}{after commands}
+% where the second and third arguments are executed before
+% and after each comment block. You can use this for global
+% formatting commands.
+% To keep definitions &c local, you can include \begingroup
+% in the `before commands' and \endgroup in the `after commands'.
+% ex:
+% \specialcomment{smalltt}
+%     {\begingroup\ttfamily\footnotesize}{\endgroup}
+% You do *not* have to do an additional
+% \includecomment{smalltt}
+% To remove 'smalltt' blocks, give \excludecomment{smalltt}
+% after the definition.
+%
+% Processing comments can apply processing to each line.
+% \processcomment{name}{each-line commands}%
+%    {before commands}{after commands}
+% By defining a control sequence 
+% \def\Thiscomment##1{...} in the before commands the user can
+% specify what is to be done with each comment line.
+% BUG this does not work quite yet BUG
+%
+% Trick for short in/exclude macros (such as \maybe{this snippet}):
+%\includecomment{cond}
+%\newcommand{\maybe}[1]{}
+%\begin{cond}
+%\renewcommand{\maybe}[1]{#1}
+%\end{cond}
+%
+% Basic approach of the implementation:
+% to comment something out, scoop up  every line in verbatim mode
+% as macro argument, then throw it away.
+% For inclusions, in LaTeX the block is written out to
+% a file \CommentCutFile (default "comment.cut"), which is
+% then included.
+% In plain TeX (and other formats) both the opening and
+% closing comands are defined as noop.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Changes in version 3.1
+% - updated author's address
+% - cleaned up some code
+% - trailing contents on \begin{env} line is always discarded
+%  even if you've done \includecomment{env}
+% - comments no longer define grouping!! you can even
+%   \includecomment{env}
+%   \begin{env}
+%   \begin{itemize}
+%   \end{env}
+%  Isn't that something ...
+% - included comments are written to file and input again.
+% Changes in 3.2
+% - \specialcomment brought up to date (thanks to Ivo Welch).
+% Changes in 3.3
+% - updated author's address again
+% - parametrised \CommentCutFile
+% Changes in 3.4
+% - added GNU public license
+% - added \processcomment, because Ivo's fix (above) brought an
+%   inconsistency to light.
+% Changes in 3.5
+% - corrected typo in header.
+% - changed author email
+% - corrected \specialcomment yet again.
+% - fixed excludecomment of an earlier defined environment.
+% Changes in 3.6
+% - The 'cut' file is now written more verbatim, using \meaning;
+%   some people reported having trouble with ISO latin 1, or umlaute.sty.
+% - removed some \newif statements.
+%   Has this suddenly become \outer again?
+%
+% Known bugs:
+% - excludecomment leads to one superfluous space
+% - processcomment leads to a superfluous line break
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\makeinnocent#1{\catcode`#1=12 }
+\def\csarg#1#2{\expandafter#1\csname#2\endcsname}
+\def\latexname{lplain}\def\latexename{LaTeX2e}
+\newwrite\CommentStream
+\def\CommentCutFile{comment.cut}
+
+\def\ProcessComment#1% start it all of
+   {\begingroup
+    \def\CurrentComment{#1}%
+    \let\do\makeinnocent \dospecials 
+    \makeinnocent\^^L% and whatever other special cases
+    \endlinechar`\^^M \catcode`\^^M=12 \xComment}
+%\def\ProcessCommentWithArg#1#2% to be used in \leveledcomment
+%   {\begingroup
+%    \def\CurrentComment{#1}%
+%    \let\do\makeinnocent \dospecials 
+%    \makeinnocent\^^L% and whatever other special cases
+%    \endlinechar`\^^M \catcode`\^^M=12 \xComment}
+{\catcode`\^^M=12 \endlinechar=-1 %
+ \gdef\xComment#1^^M{%
+    \expandafter\ProcessCommentLine}
+ \gdef\ProcessCommentLine#1^^M{\def\test{#1}
+      \csarg\ifx{End\CurrentComment Test}\test
+          \edef\next{\noexpand\EndOfComment{\CurrentComment}}%
+      \else \ThisComment{#1}\let\next\ProcessCommentLine
+      \fi \next}
+}
+
+\def\CSstringmeaning#1{\expandafter\CSgobblearrow\meaning#1}
+\def\CSstringcsnoescape#1{\expandafter\CSgobbleescape\string#1}
+{\escapechar-1
+\expandafter\expandafter\expandafter\gdef
+  \expandafter\expandafter\expandafter\CSgobblearrow
+    \expandafter\string\csname macro:->\endcsname{}
+}
+\def\CSgobbleescape#1{\ifnum`\\=`#1 \else #1\fi}
+\def\WriteCommentLine#1{\def\CStmp{#1}%
+    \immediate\write\CommentStream{\CSstringmeaning\CStmp}}
+
+% 3.1 change: in LaTeX and LaTeX2e prevent grouping
+\if 0%
+\ifx\fmtname\latexename 
+    0%
+\else \ifx\fmtname\latexname 
+          0%
+      \else 
+          1%
+\fi   \fi
+%%%%
+%%%% definitions for LaTeX
+%%%%
+\def\AfterIncludedComment
+   {\immediate\closeout\CommentStream
+    \input{\CommentCutFile}\relax
+    }%
+\def\TossComment{\immediate\closeout\CommentStream}
+\def\BeforeIncludedComment
+   {\immediate\openout\CommentStream=\CommentCutFile
+    \let\ThisComment\WriteCommentLine}
+\def\includecomment
+ #1{\message{Include comment '#1'}%
+    \csarg\let{After#1Comment}\AfterIncludedComment
+    \csarg\def{#1}{\BeforeIncludedComment
+        \ProcessComment{#1}}%
+    \CommentEndDef{#1}}
+\long\def\specialcomment
+ #1#2#3{\message{Special comment '#1'}%
+    % note: \AfterIncludedComment does \input, so #2 goes here!
+    \csarg\def{After#1Comment}{#2\AfterIncludedComment#3}%
+    \csarg\def{#1}{\BeforeIncludedComment\relax
+          \ProcessComment{#1}}%
+    \CommentEndDef{#1}}
+\long\def\processcomment
+ #1#2#3#4{\message{Lines-Processing comment '#1'}%
+    \csarg\def{After#1Comment}{#3\AfterIncludedComment#4}%
+    \csarg\def{#1}{\BeforeIncludedComment#2\relax
+          \ProcessComment{#1}}%
+    \CommentEndDef{#1}}
+\def\leveledcomment
+ #1#2{\message{Include comment '#1' up to level '#2'}%
+    %\csname #1IsLeveledCommenttrue\endcsname
+    \csarg\let{After#1Comment}\AfterIncludedComment
+    \csarg\def{#1}{\BeforeIncludedComment
+        \ProcessCommentWithArg{#1}}%
+    \CommentEndDef{#1}}
+\else 
+%%%%
+%%%%plain TeX and other formats
+%%%%
+\def\includecomment
+ #1{\message{Including comment '#1'}%
+    \csarg\def{#1}{}%
+    \csarg\def{end#1}{}}
+\long\def\specialcomment
+ #1#2#3{\message{Special comment '#1'}%
+    \csarg\def{#1}{\def\ThisComment{}\def\AfterComment{#3}#2%
+           \ProcessComment{#1}}%
+    \CommentEndDef{#1}}
+\fi
+
+%%%%
+%%%% general definition of skipped comment
+%%%%
+\def\excludecomment
+ #1{\message{Excluding comment '#1'}%
+    \csarg\def{#1}{\let\AfterComment\relax
+           \def\ThisComment####1{}\ProcessComment{#1}}%
+    \csarg\let{After#1Comment}\TossComment
+    \CommentEndDef{#1}}
+
+\if 0%
+\ifx\fmtname\latexename 
+    0%
+\else \ifx\fmtname\latexname 
+          0%
+      \else 
+          1%
+\fi   \fi
+% latex & latex2e:
+\def\EndOfComment#1{\endgroup\end{#1}%
+    \csname After#1Comment\endcsname}
+\def\CommentEndDef#1{{\escapechar=-1\relax
+    \csarg\xdef{End#1Test}{\string\\end\string\{#1\string\}}%
+    }}
+\else
+% plain & other
+\def\EndOfComment#1{\endgroup\AfterComment}
+\def\CommentEndDef#1{{\escapechar=-1\relax
+    \csarg\xdef{End#1Test}{\string\\end#1}%
+    }}
+\fi
+
+\excludecomment{comment}
+
+\endinput

examples/scholarly_paper/2021-ITP-PMTI/output/document/isabelle.sty

@@ -0,0 +1,282 @@
+%%
+%% macros for Isabelle generated LaTeX output
+%%
+
+%%% Simple document preparation (based on theory token language and symbols)
+
+% isabelle environments
+
+\newcommand{\isabellecontext}{UNKNOWN}
+\newcommand{\setisabellecontext}[1]{\def\isabellecontext{#1}}
+
+\newcommand{\isastyle}{\UNDEF}
+\newcommand{\isastylett}{\UNDEF}
+\newcommand{\isastyleminor}{\UNDEF}
+\newcommand{\isastyleminortt}{\UNDEF}
+\newcommand{\isastylescript}{\UNDEF}
+\newcommand{\isastyletext}{\normalsize\normalfont\rmfamily}
+\newcommand{\isastyletxt}{\normalfont\rmfamily}
+\newcommand{\isastylecmt}{\normalfont\rmfamily}
+
+\newcommand{\isaspacing}{%
+  \sfcode 42 1000 % .
+  \sfcode 63 1000 % ?
+  \sfcode 33 1000 % !
+  \sfcode 58 1000 % :
+  \sfcode 59 1000 % ;
+  \sfcode 44 1000 % ,
+}
+
+%symbol markup -- \emph achieves decent spacing via italic corrections
+\newcommand{\isamath}[1]{\emph{$#1$}}
+\newcommand{\isatext}[1]{\emph{#1}}
+\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}}
+\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript}
+\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
+\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript}
+\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
+\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
+
+%blackboard-bold (requires font txmia from pxfonts)
+\DeclareSymbolFont{bbbfont}{U}{txmia}{m}{it}
+\SetSymbolFont{bbbfont}{bold}{U}{txmia}{bx}{it}
+\DeclareMathSymbol{\bbbA}{\mathord}{bbbfont}{129}
+\DeclareMathSymbol{\bbbB}{\mathord}{bbbfont}{130}
+\DeclareMathSymbol{\bbbC}{\mathord}{bbbfont}{131}
+\DeclareMathSymbol{\bbbD}{\mathord}{bbbfont}{132}
+\DeclareMathSymbol{\bbbE}{\mathord}{bbbfont}{133}
+\DeclareMathSymbol{\bbbF}{\mathord}{bbbfont}{134}
+\DeclareMathSymbol{\bbbG}{\mathord}{bbbfont}{135}
+\DeclareMathSymbol{\bbbH}{\mathord}{bbbfont}{136}
+\DeclareMathSymbol{\bbbI}{\mathord}{bbbfont}{137}
+\DeclareMathSymbol{\bbbJ}{\mathord}{bbbfont}{138}
+\DeclareMathSymbol{\bbbK}{\mathord}{bbbfont}{139}
+\DeclareMathSymbol{\bbbL}{\mathord}{bbbfont}{140}
+\DeclareMathSymbol{\bbbM}{\mathord}{bbbfont}{141}
+\DeclareMathSymbol{\bbbN}{\mathord}{bbbfont}{142}
+\DeclareMathSymbol{\bbbO}{\mathord}{bbbfont}{143}
+\DeclareMathSymbol{\bbbP}{\mathord}{bbbfont}{144}
+\DeclareMathSymbol{\bbbQ}{\mathord}{bbbfont}{145}
+\DeclareMathSymbol{\bbbR}{\mathord}{bbbfont}{146}
+\DeclareMathSymbol{\bbbS}{\mathord}{bbbfont}{147}
+\DeclareMathSymbol{\bbbT}{\mathord}{bbbfont}{148}
+\DeclareMathSymbol{\bbbU}{\mathord}{bbbfont}{149}
+\DeclareMathSymbol{\bbbV}{\mathord}{bbbfont}{150}
+\DeclareMathSymbol{\bbbW}{\mathord}{bbbfont}{151}
+\DeclareMathSymbol{\bbbX}{\mathord}{bbbfont}{152}
+\DeclareMathSymbol{\bbbY}{\mathord}{bbbfont}{153}
+\DeclareMathSymbol{\bbbZ}{\mathord}{bbbfont}{154}
+
+\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
+
+\newdimen\isa@parindent\newdimen\isa@parskip
+
+\newenvironment{isabellebody}{%
+\isamarkuptrue\par%
+\isa@parindent\parindent\parindent0pt%
+\isa@parskip\parskip\parskip0pt%
+\isaspacing\isastyle}{\par}
+
+\newenvironment{isabellebodytt}{%
+\isamarkuptrue\par%
+\isa@parindent\parindent\parindent0pt%
+\isa@parskip\parskip\parskip0pt%
+\isaspacing\isastylett}{\par}
+
+\newenvironment{isabelle}
+{\begin{trivlist}\begin{isabellebody}\item\relax}
+{\end{isabellebody}\end{trivlist}}
+
+\newenvironment{isabellett}
+{\begin{trivlist}\begin{isabellebodytt}\item\relax}
+{\end{isabellebodytt}\end{trivlist}}
+
+\newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}}
+\newcommand{\isatt}[1]{\emph{\isaspacing\isastyleminortt #1}}
+
+\newcommand{\isaindent}[1]{\hphantom{#1}}
+\newcommand{\isanewline}{\mbox{}\par\mbox{}}
+\newcommand{\isasep}{}
+\newcommand{\isadigit}[1]{#1}
+
+\newcommand{\isachardefaults}{%
+\def\isacharbell{\isamath{\bigbox}}%requires stmaryrd
+\chardef\isacharbang=`\!%
+\chardef\isachardoublequote=`\"%
+\chardef\isachardoublequoteopen=`\"%
+\chardef\isachardoublequoteclose=`\"%
+\chardef\isacharhash=`\#%
+\chardef\isachardollar=`\$%
+\chardef\isacharpercent=`\%%
+\chardef\isacharampersand=`\&%
+\chardef\isacharprime=`\'%
+\chardef\isacharparenleft=`\(%
+\chardef\isacharparenright=`\)%
+\chardef\isacharasterisk=`\*%
+\chardef\isacharplus=`\+%
+\chardef\isacharcomma=`\,%
+\chardef\isacharminus=`\-%
+\chardef\isachardot=`\.%
+\chardef\isacharslash=`\/%
+\chardef\isacharcolon=`\:%
+\chardef\isacharsemicolon=`\;%
+\chardef\isacharless=`\<%
+\chardef\isacharequal=`\=%
+\chardef\isachargreater=`\>%
+\chardef\isacharquery=`\?%
+\chardef\isacharat=`\@%
+\chardef\isacharbrackleft=`\[%
+\chardef\isacharbackslash=`\\%
+\chardef\isacharbrackright=`\]%
+\chardef\isacharcircum=`\^%
+\chardef\isacharunderscore=`\_%
+\def\isacharunderscorekeyword{\_}%
+\chardef\isacharbackquote=`\`%
+\chardef\isacharbackquoteopen=`\`%
+\chardef\isacharbackquoteclose=`\`%
+\chardef\isacharbraceleft=`\{%
+\chardef\isacharbar=`\|%
+\chardef\isacharbraceright=`\}%
+\chardef\isachartilde=`\~%
+\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
+\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
+\def\isacartoucheopen{\isatext{\guilsinglleft}}%
+\def\isacartoucheclose{\isatext{\guilsinglright}}%
+}
+
+
+% keyword and section markup
+
+\newcommand{\isakeyword}[1]
+{\emph{\normalfont\bfseries\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
+\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
+\newcommand{\isacommand}[1]{\isakeyword{#1}}
+
+\newcommand{\isakeywordcontrol}[1]
+{\emph{\normalfont\bfseries\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}}
+
+\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
+\newcommand{\isamarkupsection}[1]{\section{#1}}
+\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
+\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
+\newcommand{\isamarkupparagraph}[1]{\paragraph{#1}}
+\newcommand{\isamarkupsubparagraph}[1]{\subparagraph{#1}}
+
+\newif\ifisamarkup
+\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
+\newcommand{\isaendpar}{\par\medskip}
+\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
+\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
+\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
+
+
+% index entries
+
+\newcommand{\isaindexdef}[1]{\textbf{#1}}
+\newcommand{\isaindexref}[1]{#1}
+
+
+% styles
+
+\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
+
+\newcommand{\isabellestyledefault}{%
+\def\isastyle{\small\normalfont\ttfamily\slshape}%
+\def\isastylett{\small\normalfont\ttfamily}%
+\def\isastyleminor{\small\normalfont\ttfamily\slshape}%
+\def\isastyleminortt{\small\normalfont\ttfamily}%
+\def\isastylescript{\footnotesize\normalfont\ttfamily\slshape}%
+\isachardefaults%
+}
+\isabellestyledefault
+
+\newcommand{\isabellestylett}{%
+\def\isastyle{\small\normalfont\ttfamily}%
+\def\isastylett{\small\normalfont\ttfamily}%
+\def\isastyleminor{\small\normalfont\ttfamily}%
+\def\isastyleminortt{\small\normalfont\ttfamily}%
+\def\isastylescript{\footnotesize\normalfont\ttfamily}%
+\isachardefaults%
+}
+
+\newcommand{\isabellestyleit}{%
+\def\isastyle{\small\normalfont\itshape}%
+\def\isastylett{\small\normalfont\ttfamily}%
+\def\isastyleminor{\normalfont\itshape}%
+\def\isastyleminortt{\normalfont\ttfamily}%
+\def\isastylescript{\footnotesize\normalfont\itshape}%
+\isachardefaults%
+\def\isacharunderscorekeyword{\mbox{-}}%
+\def\isacharbang{\isamath{!}}%
+\def\isachardoublequote{}%
+\def\isachardoublequoteopen{}%
+\def\isachardoublequoteclose{}%
+\def\isacharhash{\isamath{\#}}%
+\def\isachardollar{\isamath{\$}}%
+\def\isacharpercent{\isamath{\%}}%
+\def\isacharampersand{\isamath{\&}}%
+\def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}%
+\def\isacharparenleft{\isamath{(}}%
+\def\isacharparenright{\isamath{)}}%
+\def\isacharasterisk{\isamath{*}}%
+\def\isacharplus{\isamath{+}}%
+\def\isacharcomma{\isamath{\mathord,}}%
+\def\isacharminus{\isamath{-}}%
+\def\isachardot{\isamath{\mathord.}}%
+\def\isacharslash{\isamath{/}}%
+\def\isacharcolon{\isamath{\mathord:}}%
+\def\isacharsemicolon{\isamath{\mathord;}}%
+\def\isacharless{\isamath{<}}%
+\def\isacharequal{\isamath{=}}%
+\def\isachargreater{\isamath{>}}%
+\def\isacharat{\isamath{@}}%
+\def\isacharbrackleft{\isamath{[}}%
+\def\isacharbackslash{\isamath{\backslash}}%
+\def\isacharbrackright{\isamath{]}}%
+\def\isacharunderscore{\mbox{-}}%
+\def\isacharbraceleft{\isamath{\{}}%
+\def\isacharbar{\isamath{\mid}}%
+\def\isacharbraceright{\isamath{\}}}%
+\def\isachartilde{\isamath{{}\sp{\sim}}}%
+\def\isacharbackquoteopen{\isatext{\guilsinglleft}}%
+\def\isacharbackquoteclose{\isatext{\guilsinglright}}%
+}
+
+\newcommand{\isabellestyleliteral}{%
+\isabellestyleit%
+\def\isacharunderscore{\_}%
+\def\isacharunderscorekeyword{\_}%
+\chardef\isacharbackquoteopen=`\`%
+\chardef\isacharbackquoteclose=`\`%
+}
+
+\newcommand{\isabellestyleliteralunderscore}{%
+\isabellestyleliteral%
+\def\isacharunderscore{\textunderscore}%
+\def\isacharunderscorekeyword{\textunderscore}%
+}
+
+\newcommand{\isabellestylesl}{%
+\isabellestyleit%
+\def\isastyle{\small\normalfont\slshape}%
+\def\isastylett{\small\normalfont\ttfamily}%
+\def\isastyleminor{\normalfont\slshape}%
+\def\isastyleminortt{\normalfont\ttfamily}%
+\def\isastylescript{\footnotesize\normalfont\slshape}%
+}
+
+
+% cancel text
+
+\usepackage[normalem]{ulem}
+\newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}}
+
+
+% tags
+
+\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
+
+\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}

examples/scholarly_paper/2021-ITP-PMTI/output/document/isabellesym.sty

@@ -0,0 +1,496 @@
+%%
+%% definitions of standard Isabelle symbols
+%%
+
+\newcommand{\isasymzero}{\isamath{\mathbf{0}}}  %requires amssymb
+\newcommand{\isasymone}{\isamath{\mathbf{1}}}  %requires amssymb
+\newcommand{\isasymtwo}{\isamath{\mathbf{2}}}  %requires amssymb
+\newcommand{\isasymthree}{\isamath{\mathbf{3}}}  %requires amssymb
+\newcommand{\isasymfour}{\isamath{\mathbf{4}}}  %requires amssymb
+\newcommand{\isasymfive}{\isamath{\mathbf{5}}}  %requires amssymb
+\newcommand{\isasymsix}{\isamath{\mathbf{6}}}  %requires amssymb
+\newcommand{\isasymseven}{\isamath{\mathbf{7}}}  %requires amssymb
+\newcommand{\isasymeight}{\isamath{\mathbf{8}}}  %requires amssymb
+\newcommand{\isasymnine}{\isamath{\mathbf{9}}}  %requires amssymb
+\newcommand{\isasymA}{\isamath{\mathcal{A}}}
+\newcommand{\isasymB}{\isamath{\mathcal{B}}}
+\newcommand{\isasymC}{\isamath{\mathcal{C}}}
+\newcommand{\isasymD}{\isamath{\mathcal{D}}}
+\newcommand{\isasymE}{\isamath{\mathcal{E}}}
+\newcommand{\isasymF}{\isamath{\mathcal{F}}}
+\newcommand{\isasymG}{\isamath{\mathcal{G}}}
+\newcommand{\isasymH}{\isamath{\mathcal{H}}}
+\newcommand{\isasymI}{\isamath{\mathcal{I}}}
+\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
+\newcommand{\isasymK}{\isamath{\mathcal{K}}}
+\newcommand{\isasymL}{\isamath{\mathcal{L}}}
+\newcommand{\isasymM}{\isamath{\mathcal{M}}}
+\newcommand{\isasymN}{\isamath{\mathcal{N}}}
+\newcommand{\isasymO}{\isamath{\mathcal{O}}}
+\newcommand{\isasymP}{\isamath{\mathcal{P}}}
+\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
+\newcommand{\isasymR}{\isamath{\mathcal{R}}}
+\newcommand{\isasymS}{\isamath{\mathcal{S}}}
+\newcommand{\isasymT}{\isamath{\mathcal{T}}}
+\newcommand{\isasymU}{\isamath{\mathcal{U}}}
+\newcommand{\isasymV}{\isamath{\mathcal{V}}}
+\newcommand{\isasymW}{\isamath{\mathcal{W}}}
+\newcommand{\isasymX}{\isamath{\mathcal{X}}}
+\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
+\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
+\newcommand{\isasyma}{\isamath{\mathrm{a}}}
+\newcommand{\isasymb}{\isamath{\mathrm{b}}}
+\newcommand{\isasymc}{\isamath{\mathrm{c}}}
+\newcommand{\isasymd}{\isamath{\mathrm{d}}}
+\newcommand{\isasyme}{\isamath{\mathrm{e}}}
+\newcommand{\isasymf}{\isamath{\mathrm{f}}}
+\newcommand{\isasymg}{\isamath{\mathrm{g}}}
+\newcommand{\isasymh}{\isamath{\mathrm{h}}}
+\newcommand{\isasymi}{\isamath{\mathrm{i}}}
+\newcommand{\isasymj}{\isamath{\mathrm{j}}}
+\newcommand{\isasymk}{\isamath{\mathrm{k}}}
+\newcommand{\isasyml}{\isamath{\mathrm{l}}}
+\newcommand{\isasymm}{\isamath{\mathrm{m}}}
+\newcommand{\isasymn}{\isamath{\mathrm{n}}}
+\newcommand{\isasymo}{\isamath{\mathrm{o}}}
+\newcommand{\isasymp}{\isamath{\mathrm{p}}}
+\newcommand{\isasymq}{\isamath{\mathrm{q}}}
+\newcommand{\isasymr}{\isamath{\mathrm{r}}}
+\newcommand{\isasyms}{\isamath{\mathrm{s}}}
+\newcommand{\isasymt}{\isamath{\mathrm{t}}}
+\newcommand{\isasymu}{\isamath{\mathrm{u}}}
+\newcommand{\isasymv}{\isamath{\mathrm{v}}}
+\newcommand{\isasymw}{\isamath{\mathrm{w}}}
+\newcommand{\isasymx}{\isamath{\mathrm{x}}}
+\newcommand{\isasymy}{\isamath{\mathrm{y}}}
+\newcommand{\isasymz}{\isamath{\mathrm{z}}}
+\newcommand{\isasymAA}{\isamath{\mathfrak{A}}}  %requires eufrak
+\newcommand{\isasymBB}{\isamath{\mathfrak{B}}}  %requires eufrak
+\newcommand{\isasymCC}{\isamath{\mathfrak{C}}}  %requires eufrak
+\newcommand{\isasymDD}{\isamath{\mathfrak{D}}}  %requires eufrak
+\newcommand{\isasymEE}{\isamath{\mathfrak{E}}}  %requires eufrak
+\newcommand{\isasymFF}{\isamath{\mathfrak{F}}}  %requires eufrak
+\newcommand{\isasymGG}{\isamath{\mathfrak{G}}}  %requires eufrak
+\newcommand{\isasymHH}{\isamath{\mathfrak{H}}}  %requires eufrak
+\newcommand{\isasymII}{\isamath{\mathfrak{I}}}  %requires eufrak
+\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}}  %requires eufrak
+\newcommand{\isasymKK}{\isamath{\mathfrak{K}}}  %requires eufrak
+\newcommand{\isasymLL}{\isamath{\mathfrak{L}}}  %requires eufrak
+\newcommand{\isasymMM}{\isamath{\mathfrak{M}}}  %requires eufrak
+\newcommand{\isasymNN}{\isamath{\mathfrak{N}}}  %requires eufrak
+\newcommand{\isasymOO}{\isamath{\mathfrak{O}}}  %requires eufrak
+\newcommand{\isasymPP}{\isamath{\mathfrak{P}}}  %requires eufrak
+\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}}  %requires eufrak
+\newcommand{\isasymRR}{\isamath{\mathfrak{R}}}  %requires eufrak
+\newcommand{\isasymSS}{\isamath{\mathfrak{S}}}  %requires eufrak
+\newcommand{\isasymTT}{\isamath{\mathfrak{T}}}  %requires eufrak
+\newcommand{\isasymUU}{\isamath{\mathfrak{U}}}  %requires eufrak
+\newcommand{\isasymVV}{\isamath{\mathfrak{V}}}  %requires eufrak
+\newcommand{\isasymWW}{\isamath{\mathfrak{W}}}  %requires eufrak
+\newcommand{\isasymXX}{\isamath{\mathfrak{X}}}  %requires eufrak
+\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}}  %requires eufrak
+\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}}  %requires eufrak
+\newcommand{\isasymaa}{\isamath{\mathfrak{a}}}  %requires eufrak
+\newcommand{\isasymbb}{\isamath{\mathfrak{b}}}  %requires eufrak
+\newcommand{\isasymcc}{\isamath{\mathfrak{c}}}  %requires eufrak
+\newcommand{\isasymdd}{\isamath{\mathfrak{d}}}  %requires eufrak
+\newcommand{\isasymee}{\isamath{\mathfrak{e}}}  %requires eufrak
+\newcommand{\isasymff}{\isamath{\mathfrak{f}}}  %requires eufrak
+\newcommand{\isasymgg}{\isamath{\mathfrak{g}}}  %requires eufrak
+\newcommand{\isasymhh}{\isamath{\mathfrak{h}}}  %requires eufrak
+\newcommand{\isasymii}{\isamath{\mathfrak{i}}}  %requires eufrak
+\newcommand{\isasymjj}{\isamath{\mathfrak{j}}}  %requires eufrak
+\newcommand{\isasymkk}{\isamath{\mathfrak{k}}}  %requires eufrak
+\newcommand{\isasymll}{\isamath{\mathfrak{l}}}  %requires eufrak
+\newcommand{\isasymmm}{\isamath{\mathfrak{m}}}  %requires eufrak
+\newcommand{\isasymnn}{\isamath{\mathfrak{n}}}  %requires eufrak
+\newcommand{\isasymoo}{\isamath{\mathfrak{o}}}  %requires eufrak
+\newcommand{\isasympp}{\isamath{\mathfrak{p}}}  %requires eufrak
+\newcommand{\isasymqq}{\isamath{\mathfrak{q}}}  %requires eufrak
+\newcommand{\isasymrr}{\isamath{\mathfrak{r}}}  %requires eufrak
+\newcommand{\isasymss}{\isamath{\mathfrak{s}}}  %requires eufrak
+\newcommand{\isasymtt}{\isamath{\mathfrak{t}}}  %requires eufrak
+\newcommand{\isasymuu}{\isamath{\mathfrak{u}}}  %requires eufrak
+\newcommand{\isasymvv}{\isamath{\mathfrak{v}}}  %requires eufrak
+\newcommand{\isasymww}{\isamath{\mathfrak{w}}}  %requires eufrak
+\newcommand{\isasymxx}{\isamath{\mathfrak{x}}}  %requires eufrak
+\newcommand{\isasymyy}{\isamath{\mathfrak{y}}}  %requires eufrak
+\newcommand{\isasymzz}{\isamath{\mathfrak{z}}}  %requires eufrak
+\newcommand{\isasymalpha}{\isamath{\alpha}}
+\newcommand{\isasymbeta}{\isamath{\beta}}
+\newcommand{\isasymgamma}{\isamath{\gamma}}
+\newcommand{\isasymdelta}{\isamath{\delta}}
+\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
+\newcommand{\isasymzeta}{\isamath{\zeta}}
+\newcommand{\isasymeta}{\isamath{\eta}}
+\newcommand{\isasymtheta}{\isamath{\vartheta}}
+\newcommand{\isasymiota}{\isamath{\iota}}
+\newcommand{\isasymkappa}{\isamath{\kappa}}
+\newcommand{\isasymlambda}{\isamath{\lambda}}
+\newcommand{\isasymmu}{\isamath{\mu}}
+\newcommand{\isasymnu}{\isamath{\nu}}
+\newcommand{\isasymxi}{\isamath{\xi}}
+\newcommand{\isasympi}{\isamath{\pi}}
+\newcommand{\isasymrho}{\isamath{\varrho}}
+\newcommand{\isasymsigma}{\isamath{\sigma}}
+\newcommand{\isasymtau}{\isamath{\tau}}
+\newcommand{\isasymupsilon}{\isamath{\upsilon}}
+\newcommand{\isasymphi}{\isamath{\varphi}}
+\newcommand{\isasymchi}{\isamath{\chi}}
+\newcommand{\isasympsi}{\isamath{\psi}}
+\newcommand{\isasymomega}{\isamath{\omega}}
+\newcommand{\isasymGamma}{\isamath{\Gamma}}
+\newcommand{\isasymDelta}{\isamath{\Delta}}
+\newcommand{\isasymTheta}{\isamath{\Theta}}
+\newcommand{\isasymLambda}{\isamath{\Lambda}}
+\newcommand{\isasymXi}{\isamath{\Xi}}
+\newcommand{\isasymPi}{\isamath{\Pi}}
+\newcommand{\isasymSigma}{\isamath{\Sigma}}
+\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
+\newcommand{\isasymPhi}{\isamath{\Phi}}
+\newcommand{\isasymPsi}{\isamath{\Psi}}
+\newcommand{\isasymOmega}{\isamath{\Omega}}
+\newcommand{\isasymbbbA}{\isamath{\bbbA}}  %requires font txmia from txfonts
+\newcommand{\isasymbool}{\isamath{\bbbB}}  %requires font txmia from txfonts
+\newcommand{\isasymcomplex}{\isamath{\bbbC}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbD}{\isamath{\bbbD}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbE}{\isamath{\bbbE}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbF}{\isamath{\bbbF}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbG}{\isamath{\bbbG}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbH}{\isamath{\bbbH}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbI}{\isamath{\bbbI}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbJ}{\isamath{\bbbJ}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbK}{\isamath{\bbbK}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbL}{\isamath{\bbbL}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbM}{\isamath{\bbbM}}  %requires font txmia from txfonts
+\newcommand{\isasymnat}{\isamath{\bbbN}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbO}{\isamath{\bbbO}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbP}{\isamath{\bbbP}}  %requires font txmia from txfonts
+\newcommand{\isasymrat}{\isamath{\bbbQ}}  %requires font txmia from txfonts
+\newcommand{\isasymreal}{\isamath{\bbbR}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbS}{\isamath{\bbbS}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbT}{\isamath{\bbbT}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbU}{\isamath{\bbbU}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbV}{\isamath{\bbbV}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbW}{\isamath{\bbbW}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbX}{\isamath{\bbbX}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbY}{\isamath{\bbbY}}  %requires font txmia from txfonts
+\newcommand{\isasymint}{\isamath{\bbbZ}}  %requires font txmia from txfonts
+\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
+\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
+\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
+\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
+\newcommand{\isasymlonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAA}}}}  %requires amsmath
+\newcommand{\isasymlonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAA}}}}  %requires amsmath
+\newcommand{\isasymlonglonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAAA}}}}  %requires amsmath
+\newcommand{\isasymlonglonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAAA}}}}  %requires amsmath
+\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
+\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
+\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
+\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
+\newcommand{\isasymLleftarrow}{\isamath{\Lleftarrow}}  %requires amssymb
+\newcommand{\isasymRrightarrow}{\isamath{\Rrightarrow}}  %requires amssymb
+\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
+\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
+\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
+\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
+\newcommand{\isasymmapsto}{\isamath{\mapsto}}
+\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
+\newcommand{\isasymmidarrow}{\isamath{\relbar}}
+\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
+\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
+\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
+\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
+\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
+\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
+\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
+\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
+\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires amssymb
+\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}}  %requires amssymb
+\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}}  %requires amssymb
+\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}}  %requires amssymb
+\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}}  %requires amssymb
+\newcommand{\isasymrestriction}{\isamath{\restriction}}  %requires amssymb
+\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
+\newcommand{\isasymup}{\isamath{\uparrow}}
+\newcommand{\isasymUp}{\isamath{\Uparrow}}
+\newcommand{\isasymdown}{\isamath{\downarrow}}
+\newcommand{\isasymDown}{\isamath{\Downarrow}}
+\newcommand{\isasymupdown}{\isamath{\updownarrow}}
+\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
+\newcommand{\isasymlangle}{\isamath{\langle}}
+\newcommand{\isasymrangle}{\isamath{\rangle}}
+\newcommand{\isasymllangle}{\isamath{\langle\mskip-5mu\langle}}
+\newcommand{\isasymrrangle}{\isamath{\rangle\mskip-5mu\rangle}}
+\newcommand{\isasymlceil}{\isamath{\lceil}}
+\newcommand{\isasymrceil}{\isamath{\rceil}}
+\newcommand{\isasymlfloor}{\isamath{\lfloor}}
+\newcommand{\isasymrfloor}{\isamath{\rfloor}}
+\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3.3mu\mid}}}
+\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3.3mu)}}}
+\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
+\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
+\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.3mu\mid}}}
+\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.3mu\rbrace}}}
+\newcommand{\isasymlblot}{\isamath{{\langle}\mkern -3.5mu{|}}}
+\newcommand{\isasymrblot}{\isamath{{|}\mkern -3.5mu{\rangle}}}
+\newcommand{\isasymguillemotleft}{\isatext{\guillemotleft}}
+\newcommand{\isasymguillemotright}{\isatext{\guillemotright}}
+\newcommand{\isasymbottom}{\isamath{\bot}}
+\newcommand{\isasymtop}{\isamath{\top}}
+\newcommand{\isasymand}{\isamath{\wedge}}
+\newcommand{\isasymAnd}{\isamath{\bigwedge}}
+\newcommand{\isasymor}{\isamath{\vee}}
+\newcommand{\isasymOr}{\isamath{\bigvee}}
+\newcommand{\isasymforall}{\isamath{\forall\,}}
+\newcommand{\isasymexists}{\isamath{\exists\,}}
+\newcommand{\isasymnot}{\isamath{\neg}}
+\newcommand{\isasymnexists}{\isamath{\nexists\,}}  %requires amssymb
+\newcommand{\isasymcircle}{\isamath{\ocircle}}  %requires wasysym
+\newcommand{\isasymbox}{\isamath{\Box}}  %requires amssymb
+\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssymb
+\newcommand{\isasymdiamondop}{\isamath{\diamond}}
+\newcommand{\isasymsurd}{\isamath{\surd}}
+\newcommand{\isasymturnstile}{\isamath{\vdash}}
+\newcommand{\isasymTurnstile}{\isamath{\models}}
+\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
+\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
+\newcommand{\isasymstileturn}{\isamath{\dashv}}
+\newcommand{\isasymle}{\isamath{\le}}
+\newcommand{\isasymge}{\isamath{\ge}}
+\newcommand{\isasymlless}{\isamath{\ll}}
+\newcommand{\isasymggreater}{\isamath{\gg}}
+\newcommand{\isasymlesssim}{\isamath{\lesssim}}  %requires amssymb
+\newcommand{\isasymgreatersim}{\isamath{\gtrsim}}  %requires amssymb
+\newcommand{\isasymlessapprox}{\isamath{\lessapprox}}  %requires amssymb
+\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}}  %requires amssymb
+\newcommand{\isasymin}{\isamath{\in}}
+\newcommand{\isasymnotin}{\isamath{\notin}}
+\newcommand{\isasymsubset}{\isamath{\subset}}
+\newcommand{\isasymsupset}{\isamath{\supset}}
+\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
+\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
+\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}  %requires amssymb
+\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires amssymb
+\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
+\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
+\newcommand{\isasyminter}{\isamath{\cap}}
+\newcommand{\isasymInter}{\isamath{\bigcap\,}}
+\newcommand{\isasymunion}{\isamath{\cup}}
+\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
+\newcommand{\isasymsqunion}{\isamath{\sqcup}}
+\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
+\newcommand{\isasymsqinter}{\isamath{\sqcap}}
+\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires stmaryrd
+\newcommand{\isasymsetminus}{\isamath{\setminus}}
+\newcommand{\isasympropto}{\isamath{\propto}}
+\newcommand{\isasymuplus}{\isamath{\uplus}}
+\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
+\newcommand{\isasymnoteq}{\isamath{\not=}}
+\newcommand{\isasymsim}{\isamath{\sim}}
+\newcommand{\isasymdoteq}{\isamath{\doteq}}
+\newcommand{\isasymsimeq}{\isamath{\simeq}}
+\newcommand{\isasymapprox}{\isamath{\approx}}
+\newcommand{\isasymasymp}{\isamath{\asymp}}
+\newcommand{\isasymcong}{\isamath{\cong}}
+\newcommand{\isasymsmile}{\isamath{\smile}}
+\newcommand{\isasymequiv}{\isamath{\equiv}}
+\newcommand{\isasymfrown}{\isamath{\frown}}
+\newcommand{\isasymJoin}{\isamath{\Join}}  %requires amssymb
+\newcommand{\isasymbowtie}{\isamath{\bowtie}}
+\newcommand{\isasymprec}{\isamath{\prec}}
+\newcommand{\isasymsucc}{\isamath{\succ}}
+\newcommand{\isasympreceq}{\isamath{\preceq}}
+\newcommand{\isasymsucceq}{\isamath{\succeq}}
+\newcommand{\isasymparallel}{\isamath{\parallel}}
+\newcommand{\isasymParallel}{\isamath{\bigparallel}}  %requires stmaryrd
+\newcommand{\isasyminterleace}{\isamath{\interleave}}  %requires stmaryrd
+\newcommand{\isasymsslash}{\isamath{\sslash}}  %requires stmaryrd
+\newcommand{\isasymbar}{\isamath{\mid}}
+\newcommand{\isasymbbar}{\isamath{[\mskip-1.5mu]}}
+\newcommand{\isasymplusminus}{\isamath{\pm}}
+\newcommand{\isasymminusplus}{\isamath{\mp}}
+\newcommand{\isasymtimes}{\isamath{\times}}
+\newcommand{\isasymdiv}{\isamath{\div}}
+\newcommand{\isasymcdot}{\isamath{\cdot}}
+\newcommand{\isasymsqdot}{\isamath{\sbox\z@{$\centerdot$}\ht\z@=.33333\ht\z@\vcenter{\box\z@}}}  %requires amssymb
+\newcommand{\isasymstar}{\isamath{\star}}
+\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
+\newcommand{\isasymcirc}{\isamath{\circ}}
+\newcommand{\isasymdagger}{\isamath{\dagger}}
+\newcommand{\isasymddagger}{\isamath{\ddagger}}
+\newcommand{\isasymlhd}{\isamath{\lhd}}  %requires amssymb
+\newcommand{\isasymrhd}{\isamath{\rhd}}  %requires amssymb
+\newcommand{\isasymunlhd}{\isamath{\unlhd}}  %requires amssymb
+\newcommand{\isasymunrhd}{\isamath{\unrhd}}  %requires amssymb
+\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
+\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
+\newcommand{\isasymtriangle}{\isamath{\triangle}}
+\newcommand{\isasymtriangleq}{\isamath{\triangleq}}  %requires amssymb
+\newcommand{\isasymoplus}{\isamath{\oplus}}
+\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
+\newcommand{\isasymotimes}{\isamath{\otimes}}
+\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
+\newcommand{\isasymodot}{\isamath{\odot}}
+\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
+\newcommand{\isasymominus}{\isamath{\ominus}}
+\newcommand{\isasymoslash}{\isamath{\oslash}}
+\newcommand{\isasymdots}{\isamath{\dots}}
+\newcommand{\isasymcdots}{\isamath{\cdots}}
+\newcommand{\isasymSum}{\isamath{\sum\,}}
+\newcommand{\isasymProd}{\isamath{\prod\,}}
+\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
+\newcommand{\isasyminfinity}{\isamath{\infty}}
+\newcommand{\isasymintegral}{\isamath{\int\,}}
+\newcommand{\isasymointegral}{\isamath{\oint\,}}
+\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
+\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
+\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
+\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
+\newcommand{\isasymaleph}{\isamath{\aleph}}
+\newcommand{\isasymemptyset}{\isamath{\emptyset}}
+\newcommand{\isasymnabla}{\isamath{\nabla}}
+\newcommand{\isasympartial}{\isamath{\partial}}
+\newcommand{\isasymRe}{\isamath{\Re}}
+\newcommand{\isasymIm}{\isamath{\Im}}
+\newcommand{\isasymflat}{\isamath{\flat}}
+\newcommand{\isasymnatural}{\isamath{\natural}}
+\newcommand{\isasymsharp}{\isamath{\sharp}}
+\newcommand{\isasymangle}{\isamath{\angle}}
+\newcommand{\isasymcopyright}{\isatext{\normalfont\rmfamily\copyright}}
+\newcommand{\isasymregistered}{\isatext{\normalfont\rmfamily\textregistered}}
+\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
+\newcommand{\isasymonequarter}{\isatext{\normalfont\rmfamily\textonequarter}}  %requires textcomp
+\newcommand{\isasymonehalf}{\isatext{\normalfont\rmfamily\textonehalf}}  %requires textcomp
+\newcommand{\isasymthreequarters}{\isatext{\normalfont\rmfamily\textthreequarters}}  %requires textcomp
+\newcommand{\isasymordfeminine}{\isatext{\normalfont\rmfamily\textordfeminine}}
+\newcommand{\isasymordmasculine}{\isatext{\normalfont\rmfamily\textordmasculine}}
+\newcommand{\isasymsection}{\isatext{\normalfont\rmfamily\S}}
+\newcommand{\isasymparagraph}{\isatext{\normalfont\rmfamily\P}}
+\newcommand{\isasymexclamdown}{\isatext{\normalfont\rmfamily\textexclamdown}}
+\newcommand{\isasymquestiondown}{\isatext{\normalfont\rmfamily\textquestiondown}}
+\newcommand{\isasymeuro}{\isatext{\euro}}  %requires eurosym
+\newcommand{\isasympounds}{\isamath{\pounds}}
+\newcommand{\isasymyen}{\isatext{\yen}}  %requires amssymb
+\newcommand{\isasymcent}{\isatext{\textcent}}  %requires textcomp
+\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
+\newcommand{\isasymdegree}{\isatext{\normalfont\rmfamily\textdegree}}  %requires textcomp
+\newcommand{\isasymhyphen}{\isatext{\normalfont\rmfamily-}}
+\newcommand{\isasymamalg}{\isamath{\amalg}}
+\newcommand{\isasymmho}{\isamath{\mho}}  %requires amssymb
+\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssymb
+\newcommand{\isasymwp}{\isamath{\wp}}
+\newcommand{\isasymwrong}{\isamath{\wr}}
+\newcommand{\isasymacute}{\isatext{\'\relax}}
+\newcommand{\isasymindex}{\isatext{\i}}
+\newcommand{\isasymdieresis}{\isatext{\"\relax}}
+\newcommand{\isasymcedilla}{\isatext{\c\relax}}
+\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
+\newcommand{\isasymsome}{\isamath{\epsilon\,}}
+\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
+\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
+
+%Z notation
+\newcommand{\isaZhbar}[1]{\rlap{\raise.0001ex\hbox{\isamath{-}}}#1}
+\newcommand{\isaZpvbar}[1]{\ooalign{\hfil\isamath{\mapstochar\mkern 5mu}\hfil\cr#1}}
+\newcommand{\isaZfvbar}[1]{\ooalign{\hfil\isamath{\mapstochar\mkern 3mu\mapstochar\mkern 5mu}\hfil\cr#1}}
+\newcommand{\isaZdarrow}[3]{\ooalign{\isamath{#1}\hfil\cr\isamath{\mkern#3mu\isamath{#2}}}}
+\newcommand{\isasymZcomp}{\isamath{\fatsemi}}  %requires stmaryrd
+\newcommand{\isasymZinj}{\isamath{\rightarrowtail}}  %requires amssymb
+\newcommand{\isasymZpinj}{\isaZpvbar{\isamath{\rightarrowtail}}}  %requires amssymb
+\newcommand{\isasymZfinj}{\isaZfvbar{\isasymZinj}}  %requires amssymb
+\newcommand{\isasymZsurj}{\isaZdarrow{\rightarrow}{\rightarrow}{4}}  %requires amssymb
+\newcommand{\isasymZpsurj}{\isaZpvbar{\isasymZsurj}}  %requires amssymb
+\newcommand{\isasymZbij}{\isaZdarrow{\rightarrowtail}{\rightarrow}{5}}  %requires amssymb
+\newcommand{\isasymZpfun}{\isaZpvbar{\isamath{\rightarrow}}}
+\newcommand{\isasymZffun}{\isaZfvbar{\isamath{\rightarrow}}}
+\newcommand{\isasymZdres}{\isamath{\lhd}}  %requires amssymb
+\newcommand{\isasymZndres}{\isaZhbar{\isamath{\lhd}}}  %requires amssymb
+\newcommand{\isasymZrres}{\isamath{\rhd}}  %requires amssymb
+\newcommand{\isasymZnrres}{\isaZhbar{\isamath{\rhd}}}  %requires amssymb
+\newcommand{\isasymZspot}{\isamath{\bullet}}
+\newcommand{\isasymZproject}{\isamath{\upharpoonright}}  %requires amssymb
+\newcommand{\isasymZsemi}{\isatext{\raise 0.66ex\hbox{\oalign{\hfil\isamath{\scriptscriptstyle\mathrm{o}}\hfil\cr\hfil\isamath{\scriptscriptstyle\mathrm{9}}\hfil}}}}
+\newcommand{\isasymZtypecolon}{\isatext{\raise 0.6ex\hbox{\oalign{\hfil\isamath{\scriptscriptstyle\mathrm{o}}\hfil\cr\hfil\isamath{\scriptscriptstyle\mathrm{o}}\hfil}}}}
+\newcommand{\isasymZhide}{\isamath{\backslash}}
+\newcommand{\isasymZcat}{\isatext{\raise 0.8ex\hbox{\isamath{\mathchar\frown}}}}
+\newcommand{\isasymZinbag}{\isatext{\ooalign{\isamath{\sqsubset\mkern-1mu}\cr\isamath{-\mkern-1mu}\cr}}}
+
+\newcommand{\isasymhole}{\isatext{\normalfont\rmfamily\wasylozenge}}  %requires wasysym
+\newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
+\newcommand{\isasymcomment}{\isatext{\isastylecmt---}}
+\newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}
+\newcommand{\isasymopen}{\isatext{\guilsinglleft}}
+\newcommand{\isasymclose}{\isatext{\guilsinglright}}
+\newcommand{\isasymcheckmark}{\isatext{\ding{51}}}  %requires pifont
+\newcommand{\isasymcrossmark}{\isatext{\ding{55}}}  %requires pifont
+\newcommand{\isactrlmarker}{\isatext{\ding{48}}}  %requires pifont
+\newcommand{\isactrltry}{\isakeywordcontrol{try}}
+\newcommand{\isactrlcan}{\isakeywordcontrol{can}}
+\newcommand{\isactrlassert}{\isakeywordcontrol{assert}}
+\newcommand{\isactrlcancel}{\isakeywordcontrol{cancel}}
+\newcommand{\isactrlbinding}{\isakeywordcontrol{binding}}
+\newcommand{\isactrlclass}{\isakeywordcontrol{class}}
+\newcommand{\isactrlclassUNDERSCOREsyntax}{\isakeywordcontrol{class{\isacharunderscore}syntax}}
+\newcommand{\isactrlcommandUNDERSCOREkeyword}{\isakeywordcontrol{command{\isacharunderscore}keyword}}
+\newcommand{\isactrlconst}{\isakeywordcontrol{const}}
+\newcommand{\isactrlconstUNDERSCOREabbrev}{\isakeywordcontrol{const{\isacharunderscore}abbrev}}
+\newcommand{\isactrlconstUNDERSCOREname}{\isakeywordcontrol{const{\isacharunderscore}name}}
+\newcommand{\isactrlconstUNDERSCOREsyntax}{\isakeywordcontrol{const{\isacharunderscore}syntax}}
+\newcommand{\isactrlcontext}{\isakeywordcontrol{context}}
+\newcommand{\isactrlcprop}{\isakeywordcontrol{cprop}}
+\newcommand{\isactrlcterm}{\isakeywordcontrol{cterm}}
+\newcommand{\isactrlctyp}{\isakeywordcontrol{ctyp}}
+\newcommand{\isactrldir}{\isakeywordcontrol{dir}}
+\newcommand{\isactrlfile}{\isakeywordcontrol{file}}
+\newcommand{\isactrlhere}{\isakeywordcontrol{here}}
+\newcommand{\isactrlinstantiate}{\isakeywordcontrol{instantiate}}
+\newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}}
+\newcommand{\isactrllatex}{\isakeywordcontrol{latex}}
+\newcommand{\isactrllocale}{\isakeywordcontrol{locale}}
+\newcommand{\isactrlmakeUNDERSCOREjudgment}{\isakeywordcontrol{make{\isacharunderscore}judgment}}
+\newcommand{\isactrldestUNDERSCOREjudgment}{\isakeywordcontrol{dest{\isacharunderscore}judgment}}
+\newcommand{\isactrlmakeUNDERSCOREstring}{\isakeywordcontrol{make{\isacharunderscore}string}}
+\newcommand{\isactrlmasterUNDERSCOREdir}{\isakeywordcontrol{master{\isacharunderscore}dir}}
+\newcommand{\isactrlmethod}{\isakeywordcontrol{method}}
+\newcommand{\isactrlnamedUNDERSCOREtheorems}{\isakeywordcontrol{named{\isacharunderscore}theorems}}
+\newcommand{\isactrlnonterminal}{\isakeywordcontrol{nonterminal}}
+\newcommand{\isactrloracleUNDERSCOREname}{\isakeywordcontrol{oracle{\isacharunderscore}name}}
+\newcommand{\isactrlpath}{\isakeywordcontrol{path}}
+\newcommand{\isactrlpathUNDERSCOREbinding}{\isakeywordcontrol{path{\isacharunderscore}binding}}
+\newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}}
+\newcommand{\isactrlprint}{\isakeywordcontrol{print}}
+\newcommand{\isactrlprop}{\isakeywordcontrol{prop}}
+\newcommand{\isactrlscala}{\isakeywordcontrol{scala}}
+\newcommand{\isactrlscalaUNDERSCOREfunction}{\isakeywordcontrol{scala{\isacharunderscore}function}}
+\newcommand{\isactrlscalaUNDERSCOREmethod}{\isakeywordcontrol{scala{\isacharunderscore}method}}
+\newcommand{\isactrlscalaUNDERSCOREobject}{\isakeywordcontrol{scala{\isacharunderscore}object}}
+\newcommand{\isactrlscalaUNDERSCOREtype}{\isakeywordcontrol{scala{\isacharunderscore}type}}
+\newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}}
+\newcommand{\isactrlsort}{\isakeywordcontrol{sort}}
+\newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}}
+\newcommand{\isactrlsystemUNDERSCOREoption}{\isakeywordcontrol{system{\isacharunderscore}option}}
+\newcommand{\isactrlterm}{\isakeywordcontrol{term}}
+\newcommand{\isactrltheory}{\isakeywordcontrol{theory}}
+\newcommand{\isactrltheoryUNDERSCOREcontext}{\isakeywordcontrol{theory{\isacharunderscore}context}}
+\newcommand{\isactrltyp}{\isakeywordcontrol{typ}}
+\newcommand{\isactrltypeUNDERSCOREabbrev}{\isakeywordcontrol{type{\isacharunderscore}abbrev}}
+\newcommand{\isactrltypeUNDERSCOREname}{\isakeywordcontrol{type{\isacharunderscore}name}}
+\newcommand{\isactrltypeUNDERSCOREsyntax}{\isakeywordcontrol{type{\isacharunderscore}syntax}}
+\newcommand{\isactrlundefined}{\isakeywordcontrol{undefined}}
+\newcommand{\isactrltvar}{\isakeywordcontrol{tvar}}
+\newcommand{\isactrlvar}{\isakeywordcontrol{var}}
+\newcommand{\isactrlConst}{\isakeywordcontrol{Const}}
+\newcommand{\isactrlConstUNDERSCORE}{\isakeywordcontrol{Const{\isacharunderscore}}}
+\newcommand{\isactrlConstUNDERSCOREfn}{\isakeywordcontrol{Const{\isacharunderscore}fn}}
+\newcommand{\isactrlType}{\isakeywordcontrol{Type}}
+\newcommand{\isactrlTypeUNDERSCOREfn}{\isakeywordcontrol{Type{\isacharunderscore}fn}}
+
+\newcommand{\isactrlcode}{\isakeywordcontrol{code}}
+\newcommand{\isactrlcomputation}{\isakeywordcontrol{computation}}
+\newcommand{\isactrlcomputationUNDERSCOREconv}{\isakeywordcontrol{computation{\isacharunderscore}conv}}
+\newcommand{\isactrlcomputationUNDERSCOREcheck}{\isakeywordcontrol{computation{\isacharunderscore}check}}
+\newcommand{\isactrlifUNDERSCORElinux}{\isakeywordcontrol{if{\isacharunderscore}linux}}
+\newcommand{\isactrlifUNDERSCOREmacos}{\isakeywordcontrol{if{\isacharunderscore}macos}}
+\newcommand{\isactrlifUNDERSCOREwindows}{\isakeywordcontrol{if{\isacharunderscore}windows}}
+\newcommand{\isactrlifUNDERSCOREunix}{\isakeywordcontrol{if{\isacharunderscore}unix}}

examples/scholarly_paper/2021-ITP-PMTI/output/document/isabelletags.sty

@@ -0,0 +1,20 @@
+%plain TeX version of comment package -- much faster!
+\let\isafmtname\fmtname\def\fmtname{plain}
+\usepackage{comment}
+\let\fmtname\isafmtname
+
+\newcommand{\isakeeptag}[1]%
+{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
+\newcommand{\isadroptag}[1]%
+{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
+\newcommand{\isafoldtag}[1]%
+{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
+
+\isakeeptag{ML}
+\isakeeptag{document}
+\isakeeptag{important}
+\isadroptag{invisible}
+\isakeeptag{proof}
+\isakeeptag{theory}
+\isakeeptag{unimportant}
+\isakeeptag{visible}

examples/scholarly_paper/2021-ITP-PMTI/output/document/isadof.cfg

@@ -0,0 +1,2 @@
+Template: lncs
+Ontology: scholarly_paper

examples/scholarly_paper/2021-ITP-PMTI/output/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/2021-ITP-PMTI/output/document/pdfsetup.sty

@@ -0,0 +1,7 @@
+%%
+%% default hyperref setup (both for pdf and dvi output)
+%%
+
+\usepackage{color}
+\definecolor{linkcolor}{rgb}{0,0,0.5}
+\usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor,filecolor=linkcolor,urlcolor=linkcolor,pdfpagelabels]{hyperref}

examples/scholarly_paper/2021-ITP-PMTI/output/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}

examples/scholarly_paper/2021-ITP-PMTI/output/document/session.tex

@@ -0,0 +1 @@
+\input{paper.tex}

src/document-templates/root-lncs.tex

@@ -98,7 +98,7 @@
 \input{session}
 % optional bibliography
 \IfFileExists{root.bib}{%
-{\small   \renewcommand{\doi}[1]{}
+{\small  
   \newcommand{\urlprefix}{}
 
   \bibliographystyle{splncs04}

src/ontologies/CENELEC_50128/CENELEC_50128.thy

@@ -272,34 +272,36 @@ NOTE Verification is mostly based on document reviews (design, implementation, t
 Definition*[verifier, short_name="''verifier''"]
 \<open>entity that is responsible for one or more verification activities\<close>
 
+chapter\<open>Software Management and Organisation\<close>
+text\<open>Representing chapter 5 in @{cite "bsi:50128:2014"}.\<close>
 
 section\<open>Organization, Roles and Responsabilities\<close>
 text\<open>see also section \<^emph>\<open>Software management and organization\<close>.\<close>
 
-datatype role =  PM  (* Program Manager *) 
-              |  RQM (* Requirements Manager *)
-              |  DES (* Designer *)
-              |  IMP (* Implementer *)
-              |  ASR (* Assessor *)
-              |  INT (* Integrator *)
-              |  TST (* Tester *)
-              |  VER (* Verifier *)
-              |  VnV (* Verification and Validation *)
-              |  VAL (* Validator *)
+datatype role =  PM     \<comment> \<open>Program Manager\<close>
+              |  RQM    \<comment> \<open>Requirements Manager\<close> 
+              |  DES    \<comment> \<open>Designer\<close>
+              |  IMP    \<comment> \<open>Implementer\<close> 
+              |  ASR    \<comment> \<open>Assessor\<close> 
+              |  INT    \<comment> \<open>Integrator\<close> 
+              |  TST    \<comment> \<open>Tester\<close>
+              |  VER    \<comment> \<open>Verifier\<close>
+              |  VnV    \<comment> \<open>Verification and Validation\<close>
+              |  VAL    \<comment> \<open>Validator\<close>
 
 
 
-datatype phase = SYSDEV_ext (* System Development Phase (external) *) 
-               | SPl   (* Software Planning *)
-               | SR    (* Software Requirement      *) 
-               | SA    (* Software Architecture     *)
-               | SDES  (* Software Design           *)
-               | SCDES (* Software Component Design *)
-               | CInT  (* Component Implementation and Testing *)
-               | SI    (* Software Integration      *)
-               | SV    (* Software Validation       *)
-               | SD    (* Software Deployment       *)
-               | SM    (* Software Maintenance      *)
+datatype phase = SYSDEV_ext \<comment> \<open> System Development Phase (external)\<close>  
+               | SPl   \<comment> \<open>Software Planning\<close>
+               | SR    \<comment> \<open>Software Requirement\<close> 
+               | SA    \<comment> \<open>Software Architecture\<close>
+               | SDES  \<comment> \<open>Software Design\<close>
+               | SCDES \<comment> \<open>Software Component Design\<close> 
+               | CInT  \<comment> \<open>Component Implementation and Testing\<close>
+               | SI    \<comment> \<open>Software Integration\<close>
+               | SV    \<comment> \<open>Software Validation\<close>
+               | SD    \<comment> \<open>Software Deployment\<close>
+               | SM    \<comment> \<open>Software Maintenance\<close>
 
 abbreviation software_requirement      :: "phase" where "software_requirement  \<equiv> SR"
 abbreviation software_architecture     :: "phase" where "software_architecture \<equiv> SA"
@@ -429,6 +431,21 @@ doc_class TC = requirement +
    is_concerned :: "role set" <= "UNIV" 
    type_synonym timing_constraint = TC
 
+
+section\<open>Personal Competence\<close>
+
+text\<open>pp. 20 MORE TO COME\<close>
+
+section\<open>Lifecycle Issues and Documentation\<close>
+
+text\<open>Figure 3 in Chapter 5: Illustrative Development Lifecycle 1\<close>
+
+text\<open>Global Overview\<close>
+
+figure*[fig3::figure, relative_width="100", 
+ src="''examples/CENELEC_50128/mini_odo/document/figures/CENELEC-Fig.3-docStructure.png''"]
+\<open>Illustrative Development Lifecycle 1\<close>
+                                     
 section\<open>Software Assurance related Entities and Concepts\<close>
 
 
@@ -494,121 +511,145 @@ doc_class judgement =
 
 section\<open> Design and Test Documents \<close> 
 
-doc_class cenelec_text = text_element +
+doc_class cenelec_document = text_element +
    phase        :: "phase"
+   level        :: "int option" <= "Some(0)" 
+   written_by   :: role                       \<comment> \<open>Annex C Table C.1 \<close>
+   fst_check    :: role                       \<comment> \<open>Annex C Table C.1\<close>
+   snd_check    :: role                       \<comment> \<open>Annex C Table C.1\<close>
    is_concerned :: "role set" <= "UNIV" 
+   invariant must_be_chapter :: "text_element.level \<sigma> = Some(0)" 
+   invariant three_eyes_prcpl:: "  written_by \<sigma> \<noteq> fst_check \<sigma> 
+                                 \<and> written_by \<sigma> \<noteq> snd_check \<sigma>"
+text\<open>see Fig.3.\<close>
 
 
-
-doc_class SYSREQS = cenelec_text + 
+doc_class SYSREQS = cenelec_document + 
    phase        :: "phase"  <= "SYSDEV_ext" 
-   accepts      "\<lbrace>objectives||requirement||cenelec_text\<rbrace>\<^sup>+ "       
+   accepts      "\<lbrace>objectives||requirement||cenelec_document\<rbrace>\<^sup>+ "       
    type_synonym system_requirements_specification = SYSREQS
 
-doc_class SYSSREQS = cenelec_text + 
+doc_class SYSSREQS = cenelec_document + 
    phase        :: "phase"  <= "SYSDEV_ext" 
    type_synonym system_safety_requirements_specification = SYSSREQS
 
-doc_class SYSAD = cenelec_text + 
+doc_class SYSAD = cenelec_document + 
    phase        :: "phase"  <= "SYSDEV_ext" 
    type_synonym system_architecture_description = SYSAD
 
-doc_class SYSS_pl = cenelec_text + 
+doc_class SYSS_pl = cenelec_document + 
    phase        :: "phase"  <= "SPl" 
    type_synonym system_safety_plan = SYSS_pl
 
-doc_class SYS_VnV_pl = cenelec_text + 
+doc_class SYS_VnV_pl = cenelec_document + 
    phase        :: "phase"  <= "SPl" 
    type_synonym system_VnV_plan = SYS_VnV_pl
 
-doc_class SWRS = cenelec_text + 
+doc_class SWRS = cenelec_document + 
    phase        :: "phase"  <= "SD" 
    type_synonym software_requirements_specification = SWRS
 
-doc_class SWRVR = cenelec_text + 
+doc_class SWRVR = cenelec_document + 
    phase        :: "phase"  <= "SD" 
    type_synonym software_requirements_verification_report = SWRVR
 
 
-doc_class SWTS = cenelec_text + 
+doc_class SWTS = cenelec_document + 
    phase        :: "phase"  <= "SD" 
    type_synonym software_test_specification = SWTS
 
-doc_class SWAS = cenelec_text + 
+   
+doc_class SWAS = cenelec_document + 
    phase        :: "phase"  <= "SD" 
    type_synonym software_architecture_specification = SWAS
 
-doc_class SWDS = cenelec_text + 
+doc_class SWDS = cenelec_document + 
    phase        :: "phase"  <= "SD" 
    type_synonym software_design_specification = SWDS
 
-doc_class SWIS = cenelec_text + 
-   phase        :: "phase"  <= "SD" 
+doc_class SWIS_E =
+   \<comment> \<open>input - output of an operation; alternatives could be channels or public global variables ...\<close>
+   op_name           :: "string"
+   op_args_ty        :: "(string \<times> typ) list \<times> typ"
+   raises_exn        :: "(string \<times> typ) list"         \<comment> \<open>exn name and value\<close>
+   pre_cond          :: "(string \<times> thm) list" <= "[]" \<comment> \<open>labels and predicates\<close>
+   post_cond         :: "(string \<times> thm) list" <= "[]" \<comment> \<open>labels and predicates\<close>
+   boundary_pre_cond :: "thm list" <= "[]"
+   type_synonym software_interface_specification_element = SWIS_E
+
+
+doc_class SWIS = cenelec_document + 
+   phase        :: "phase"  <= "SCDES" 
+   written_by   :: "role"   <= "DES"
+   fst_check    :: "role"   <= "VER"
+   snd_check    :: "role"   <= "VAL"
+   components   :: "SWIS_E list"
    type_synonym software_interface_specification = SWIS
 
-doc_class SWITS = cenelec_text + 
+doc_class SWITS = cenelec_document + 
    phase        :: "phase"  <= "SD" 
    type_synonym software_integration_test_specification = SWITS
 
-doc_class SWHITS = cenelec_text + 
+doc_class SWHITS = cenelec_document + 
    phase        :: "phase"  <= "SD" 
    type_synonym software_hardware_integration_test_specification = SWHITS
 
-doc_class SWADVR = cenelec_text + 
+doc_class SWADVR = cenelec_document + 
    phase        :: "phase"  <= "SD" 
    type_synonym software_architecture_and_design_verification_report = SWADVR
 
-doc_class SWCDS = cenelec_text + 
+doc_class SWCDS = cenelec_document + 
    phase        :: "phase"  <= "SD" 
    type_synonym software_component_design_specification = SWCDS
 
-doc_class SWCTS = cenelec_text + 
+doc_class SWCTS = cenelec_document + 
    phase        :: "phase"  <= "SD" 
    type_synonym software_component_test_specification = SWCTS
 
-doc_class SWCDVR = cenelec_text + 
+doc_class SWCDVR = cenelec_document + 
    phase        :: "phase"  <= "SD" 
    type_synonym software_component_design_verification_report = SWCDVR
 
 
-doc_class SWSCD = cenelec_text + 
+doc_class SWSCD = cenelec_document + 
    phase        :: "phase"  <= "SD" 
    type_synonym software_source_code_and_documentation = SWSCD
 
-doc_class SWCTR = cenelec_text + 
+doc_class SWCTR = cenelec_document + 
    phase        :: "phase"  <= "SD" 
    type_synonym software_component_test_report = SWCTR
 
-doc_class SWSCVR = cenelec_text + 
+doc_class SWSCVR = cenelec_document + 
    phase        :: "phase"  <= "SD" 
    type_synonym software_source_code_verification_report = SWSCVR
 
-doc_class SWHAITR = cenelec_text +
+doc_class SWHAITR = cenelec_document +
    phase        :: "phase"  <= "SD" 
    type_synonym software_hardware_integration_test_report = SWHAITR
 
-doc_class SWIVR = cenelec_text +
+doc_class SWIVR = cenelec_document +
    phase        :: "phase"  <= "SD" 
    type_synonym software_integration_verification_report = SWIVR
 
-doc_class SWTR_global = cenelec_text + 
+doc_class SWTR_global = cenelec_document + 
    phase        :: "phase"  <= "SD" 
    type_synonym overall_software_test_report = SWTR_global
 
-doc_class SWVALR = cenelec_text +
+doc_class SWVALR = cenelec_document +
    phase        :: "phase"  <= "SD" 
    type_synonym software_validation_report = SWVALR
 
-doc_class SWDD = cenelec_text + 
+doc_class SWDD = cenelec_document + 
    phase        :: "phase"  <= "SD" 
    type_synonym software_deployment_documents = SWDD
 
-doc_class SWMD = cenelec_text + 
+doc_class SWMD = cenelec_document + 
    phase        :: "phase"  <= "SD" 
    type_synonym software_maintenance_documents = SWMD
 
  
 section\<open> Software Assurance \<close>
+\<comment> \<open>MORE TO COME\<close>
 
 subsection\<open> Software Testing \<close>
 text\<open>Objective: 
@@ -725,20 +766,26 @@ doc_class test_requirement = test_item +
 doc_class test_adm_role = test_item +
              name :: string
 
-doc_class test_documentation = 
+doc_class test_documentation =    (* OUTDATED ? *)
              no :: "nat"
              accepts "test_specification ~~ 
                       \<lbrace>test_case~~test_result\<rbrace>\<^sup>+ ~~ 
                       \<lbrace>test_environment||test_tool\<rbrace>\<^sup>+ ~~
                       \<lbrakk>test_requirement\<rbrakk>  ~~ 
                       test_adm_role"
-             accepts "test_specification ~~ 
-                      \<lbrace>test_case~~test_result\<rbrace>\<^sup>+ ~~ 
-                      \<lbrace>test_environment||test_tool\<rbrace>\<^sup>+ ~~
-                      \<lbrakk>test_requirement \<rbrakk> ~~ 
-                      test_adm_role"
 
 
+section\<open>Global Documentation Structure\<close>
+
+doc_class global_documentation_structure = text_element +
+   level :: "int option" <= "Some(-1::int)"  \<comment> \<open>document must be a chapter\<close>
+   accepts "SYSREQS      ~~                  \<comment> \<open>system_requirements_specification\<close>
+            SYSSREQS     ~~                  \<comment> \<open>system_safety_requirements_specification\<close> 
+            SYSAD        ~~                  \<comment> \<open>system_architecture description\<close>
+            SYSS_pl      ~~                  \<comment> \<open>system safety plan\<close> 
+            (SWRS || SWTS)  "                \<comment> \<open>software requirements specification OR
+                                                 overall software test specification\<close> 
+(* MORE TO COME : *)
 
 section\<open> META : Testing and Validation \<close>
 

src/tests/Mapped_PILIB_Ontology.thy

@@ -0,0 +1,197 @@
+theory Mapped_PILIB_Ontology
+  imports "Isabelle_DOF.Isa_DOF"
+
+
+begin
+
+
+define_shortcut* hol      \<rightleftharpoons> \<open>HOL\<close>
+                 isabelle \<rightleftharpoons> \<open>Isabelle/HOL\<close>
+                 dof      \<rightleftharpoons> \<open>Isabelle/DOF\<close>
+                 LaTeX    \<rightleftharpoons> \<open>LaTeX\<close>
+                 html     \<rightleftharpoons> \<open>HTML\<close>
+                 csp      \<rightleftharpoons> \<open>CSP\<close>      \<comment>\<open>obsolete\<close>
+                 holcsp   \<rightleftharpoons> \<open>HOL-CSP\<close>  \<comment>\<open>obsolete\<close> 
+
+
+
+
+term\<open>fold (+) S 0\<close>  
+
+definition sum 
+  where "sum S = (fold (+) S 0)"
+
+datatype Hardware_Type = 
+  Motherboard | 
+  Expansion_Card | 
+  Storage_Device | 
+  Fixed_Media | 
+  Removable_Media |
+  Input_Device |
+  Output_Device
+
+text\<open>
+\<^dof> framework does not assume that all documents reference the same ontology. 
+Each document may build its local ontology without any external reference. 
+It may also build it based upon one or several reference ontologies (i.e., standard ones). 
+
+The relationship between the local ontology and the reference one is formalised using a morphism function. 
+More precisely, a class of a local ontology may be described as a consequence of a transformation applied
+to one or several other class(es) defined in other ontologies. This means that each instance of the former can be 
+computed from one or more instances of the latter. 
+
+
+Thanks to the morphism relationship, the obtained class may either import properties (definitions are preserved) 
+or map properties (the properties are different but are semantically equivalent) that are defined in the referenced class(es). 
+It may also define additional properties.
+\<close>
+
+(* Reference Ontology *)
+onto_class Resource =
+  name :: string
+
+onto_class Electronic = Resource +
+  provider :: string
+  manufacturer :: string
+
+onto_class Component = Electronic +
+  mass :: int
+  dimensions :: "int list" 
+
+onto_class Simulation_Model = Electronic +
+  type :: string
+
+onto_class Informatic = Resource +
+  description :: string
+
+onto_class Hardware = Informatic +
+  type :: Hardware_Type
+  mass :: int
+  composed_of :: "Component list" 
+  invariant c1 :: "mass \<sigma> = sum(map Component.mass (composed_of \<sigma>))"
+
+onto_class R_Software = Informatic +
+  version :: int
+
+text\<open>
+To illustrate this process, we use the reference ontology (considered as a standard) described 
+in the listing X, defining the Resource, Electronic, Component, Informatic, Hardware and Software 
+concepts (or classes). Each class contains a set of attributes or properties and some local 
+invariants. 
+
+In our example, we focus on the Hardware class containing a mass attribute and composed of a list 
+of components with a mass attribute formalising the mass value of each component. The Hardware 
+class also contains a local invariant ''c1'' to define a constraint linking the global mass of 
+a Hardware object with the masses of its own components.  
+\<close>
+
+(* Local Ontology *)
+onto_class Item =
+  name :: string
+
+onto_class Product = Item +
+  serial_number :: int
+  provider :: string
+  mass :: int
+
+onto_class Computer_Software = Item +
+  version :: int
+
+onto_class Electronic_Component = Product +
+  dimensions :: "int set"
+
+onto_class Computer_Hardware = Product +
+  type :: Hardware_Type
+  composed_of :: "Product list" 
+  invariant c2 :: "Product.mass \<sigma> = sum(map Product.mass (composed_of \<sigma>))"
+
+text\<open>
+For the needs of our document, we have defined a simple ontology to classify Software and Hardware 
+objects. This ontology is described in listing X and defines the Item, Product, Computer_Software 
+and Computer_Hardware concepts. As for the reference ontology, we focus on the Computer_Hardware 
+class defined as a list of products characterised by their mass value. This class contains a local 
+invariant ''c2'' to guarantee that its own mass value equals the sum of all the masses of the products 
+composing the object.
+\<close>
+
+definition Item_to_Resource_morphism :: "'a Item_scheme \<Rightarrow> Resource" 
+           ("_ \<langle>Resource\<rangle>\<^sub>I\<^sub>t\<^sub>e\<^sub>m" [1000]999)
+  where    "\<sigma> \<langle>Resource\<rangle>\<^sub>I\<^sub>t\<^sub>e\<^sub>m =  \<lparr>  Resource.tag_attribute = 0::int , 
+                                 Resource.name = name \<sigma> \<rparr>" 
+  
+definition Product_to_Component_morphism :: "'a Product_scheme \<Rightarrow> Component"
+           ("_ \<langle>Component\<rangle>\<^sub>P\<^sub>r\<^sub>o\<^sub>d\<^sub>u\<^sub>c\<^sub>t" [1000]999)
+  where "  \<sigma> \<langle>Component\<rangle>\<^sub>P\<^sub>r\<^sub>o\<^sub>d\<^sub>u\<^sub>c\<^sub>t = \<lparr> Resource.tag_attribute = 1::int ,
+                                 Resource.name = name \<sigma> ,
+                                 Electronic.provider  = Product.provider \<sigma> ,
+                                 Electronic.manufacturer  = ''no manufacturer'' ,
+                                 Component.mass = Product.mass \<sigma> ,
+                                 Component.dimensions = [] \<rparr>" 
+
+definition Computer_Hardware_to_Hardware_morphism :: "'a Computer_Hardware_scheme \<Rightarrow> Hardware"
+           ("_ \<langle>Hardware\<rangle>\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e" [1000]999)
+           where "\<sigma> \<langle>Hardware\<rangle>\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e =
+                  \<lparr>  Resource.tag_attribute = 2::int ,
+                     Resource.name = name \<sigma> ,
+                     Informatic.description = ''no description'', 
+                     Hardware.type = Computer_Hardware.type \<sigma> ,
+                     Hardware.mass = mass \<sigma> ,
+                     Hardware.composed_of = map Product_to_Component_morphism 
+                                                (Computer_Hardware.composed_of \<sigma>)
+                   \<rparr>" 
+
+
+text\<open>
+To check the coherence of our local ontology, we define a relationship between the local ontology 
+and the reference ontology using morphism functions (or mapping rules). These rules are applied to 
+define the relationship between one class of the local ontology to one or several other class(es) 
+described in the reference ontology. 
+
+For example,\<open>Product_to_Component_morphism\<close> and \<open>Computer_Hardware_to_Hardware_morphism\<close> definitions,
+detailed in the figure Z, specify how \<open>Product\<close> or \<open>Computer_Hardware\<close> objects are mapped to \<open>Component\<close> 
+or \<open>Hardware\<close> objects defined in the reference ontology. This mapping shows that the structure 
+of a (user) ontology may be quite different from the one of a standard ontology she references. 
+\<close>
+
+
+
+
+find_theorems Hardware.composed_of
+
+find_theorems Hardware.mass
+
+find_theorems map "(o)"
+
+
+lemma inv_c2_preserved :
+  "c2_inv \<sigma> \<Longrightarrow> c1_inv (\<sigma> \<langle>Hardware\<rangle>\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e)"
+  unfolding c1_inv_def c2_inv_def 
+            Computer_Hardware_to_Hardware_morphism_def Product_to_Component_morphism_def  
+  by (auto simp: comp_def)
+
+lemma Computer_Hardware_to_Hardware_morphism_total :
+  "Computer_Hardware_to_Hardware_morphism ` ({X::Computer_Hardware. c2_inv X}) \<subseteq> ({X::Hardware. c1_inv X})"
+  using inv_c2_preserved 
+  by auto
+
+
+
+
+declare[[invariants_checking]]
+declare[[invariants_checking_with_tactics]]
+
+text*[c1::Component, mass=4]\<open>\<close>
+text*[c2::Component, mass=4]\<open>\<close>
+
+text*[h1::Hardware, mass=8, composed_of="[@{Component \<open>c1\<close>},@{Component \<open>c2\<close>}]"]\<open>\<close>
+text*[h2::Hardware, mass=8, composed_of="[@{Component \<open>c1\<close>},@{Component \<open>c2\<close>}]"]\<open>\<close>
+
+value*\<open>
+sum (map Component.mass [@{Component \<open>c1\<close>},@{Component \<open>c2\<close>}])
+\<close>
+
+value*\<open>
+@{Hardware \<open>h1\<close>} = @{Hardware \<open>h2\<close>}
+\<close>
+
+end

src/tests/OntoMathPro_Ontology.thy

@@ -0,0 +1,75 @@
+theory OntoMathPro_Ontology
+  imports "Isabelle_DOF.Isa_DOF"
+begin
+
+datatype dc = creator string | title string
+
+datatype owl =
+    backwardCompatibleWith string
+  | deprecated string
+  | incompatibleWith string
+  | priorVersion string
+  | versionInfo string
+  
+datatype rdfs =
+    comment string
+  | isDefinedBy string
+  | label string
+  | seeAlso string
+
+datatype annotation = DC dc | OWL owl |  RDFS rdfs
+
+
+onto_class Top =
+  Annotations :: "annotation list"
+
+onto_class Field_of_mathematics =
+  Annotations :: "annotation list"
+  invariant restrict_annotation_F ::"set (Annotations \<sigma>) \<subseteq>
+                                              range (RDFS o label) \<union> range (RDFS o comment)"
+
+onto_class Mathematical_knowledge_object =
+  Annotations :: "annotation list"
+  invariant restrict_annotation_M ::"set (Annotations \<sigma>) \<subseteq>
+                                              range (RDFS o label) \<union> range (RDFS o comment)"
+
+onto_class assoc_F_M =
+  contains:: "(Field_of_mathematics \<times> Mathematical_knowledge_object) set"
+  invariant contains_defined :: "\<forall> x. x \<in> Domain (contains \<sigma>)
+                                              \<longrightarrow> (\<exists> y \<in> Range (contains \<sigma>). (x, y) \<in> contains \<sigma>)"
+
+onto_class assoc_M_F =
+  belongs_to :: "(Mathematical_knowledge_object \<times> Field_of_mathematics) set"
+  invariant belong_to_defined :: "\<forall> x. x \<in> Domain (belongs_to \<sigma>)
+                                           \<longrightarrow> (\<exists> y \<in> Range (belongs_to \<sigma>). (x, y) \<in> belongs_to \<sigma>)"
+
+onto_class assoc_M_M =
+  is_defined_by :: "(Mathematical_knowledge_object \<times> Mathematical_knowledge_object) set"
+  invariant is_defined_by_defined :: "\<forall> x. x \<in> Domain (is_defined_by \<sigma>)
+                                    \<longrightarrow> (\<exists> y \<in> Range (is_defined_by \<sigma>). (x, y) \<in> is_defined_by \<sigma>)"
+
+onto_class assoc_M_M' =
+  "defines" :: "(Mathematical_knowledge_object \<times> Mathematical_knowledge_object) set"
+  invariant defines_defined :: "\<forall> x. x \<in> Domain (defines \<sigma>)
+                                    \<longrightarrow> (\<exists> y \<in> Range (defines \<sigma>). (x, y) \<in> defines \<sigma>)"
+
+onto_class assoc_M_M_see_also =
+  see_also :: "(Mathematical_knowledge_object rel) set" 
+  invariant see_also_trans :: "\<forall> r \<in> (see_also \<sigma>). trans r"
+  invariant see_also_sym :: "\<forall> r \<in> (see_also \<sigma>). sym r"
+
+onto_class Problem = Mathematical_knowledge_object +
+  Annotations :: "annotation list"
+  
+onto_class Method = Mathematical_knowledge_object +
+  Annotations :: "annotation list"
+
+onto_class assoc_Problem_Method =
+  is_solved_by :: "(Problem \<times> Method) set"
+  invariant is_solved_by_defined :: "\<forall> x. x \<in> Domain (is_solved_by \<sigma>)
+                                    \<longrightarrow> (\<exists> y \<in> Range (is_solved_by \<sigma>). (x, y) \<in> is_solved_by \<sigma>)"
+
+onto_class assoc_Method_Problem =
+  solves :: "(Method \<times> Problem) set"
+  invariant solves_defined :: "\<forall> x. x \<in> Domain (solves \<sigma>)
+                                    \<longrightarrow> (\<exists> y \<in> Range (solves \<sigma>). (x, y) \<in> solves \<sigma>)"

src/tests/Ontology_Matching_Example.thy

@@ -9,44 +9,44 @@ text\<open>Using HOL, we can define a mapping between two ontologies.
   Here is an example which show how to map two classes.
   HOL also allows us to map the invariants (ontological rules) of the classes!\<close>
 
-type_synonym UTF8 = string
+type_synonym UTF8 = string        \<comment> \<open>for the sake of the demonstration\<close>
 
 definition utf8_to_string
-  where "utf8_to_string x = x"
+  where "utf8_to_string x = x"    \<comment> \<open>for the sake of the demonstration\<close>
 
 
 doc_class A =
-  first_name :: UTF8
-  last_name :: UTF8
-  age :: nat
-  married_to :: "string option"
+  first_name  :: UTF8
+  last_name   :: UTF8
+  age         :: nat
+  married_to  :: "string option"
   invariant a :: "age \<sigma> < 18 \<longrightarrow> married_to \<sigma> = None"
+
 doc_class B =
-  name :: string 
-  adult :: bool
-  is_married :: bool
+  name        :: string 
+  adult       :: bool
+  is_married  :: bool
   invariant b :: "is_married \<sigma> \<longrightarrow> adult \<sigma>"
 
-text\<open>We define the mapping between the two classes,
-  i.e. how to transform the class @{doc_class A} in to the class @{doc_class B}:\<close>
+text\<open>We define the mapping between the two classes,  i.e. how to transform 
+     the class @{doc_class A} in to the class @{doc_class B}:\<close>
 
-definition A_to_B_morphism
-  where "A_to_B_morphism X =
-        \<lparr> tag_attribute = A.tag_attribute X
-          , name = utf8_to_string (first_name X) @ '' ''  @ utf8_to_string (last_name X)
-          , adult = (age X \<ge> 18)
-          , is_married = (married_to X \<noteq> None) \<rparr>" 
+
+definition A_to_B_mapping :: "'a A_scheme \<Rightarrow> B" ("_ \<langle>B\<rangle>\<^sub>A" [1000]999)
+  where "\<sigma> \<langle>B\<rangle>\<^sub>A =
+        \<lparr> tag_attribute = A.tag_attribute \<sigma>
+          , name = utf8_to_string (first_name \<sigma>) @ '' ''  @ utf8_to_string (last_name \<sigma>)
+          , adult = (age \<sigma> \<ge> 18)
+          , is_married = (married_to \<sigma> \<noteq> None) \<rparr>" 
 
 text\<open>Now we check that the invariant is preserved through the morphism:\<close>
 
 lemma inv_a_preserved :
-  "a_inv X \<Longrightarrow> b_inv (A_to_B_morphism X)"
-  unfolding a_inv_def b_inv_def A_to_B_morphism_def
-  by auto
+  "a_inv \<sigma> \<Longrightarrow> b_inv (\<sigma> \<langle>B\<rangle>\<^sub>A)"
+  unfolding a_inv_def b_inv_def A_to_B_mapping_def  by auto
 
 lemma A_morphism_B_total :
-  "A_to_B_morphism ` ({X::A. a_inv X}) \<subseteq> ({X::B. b_inv X})"
-  using inv_a_preserved
-  by auto
+  "A_to_B_mapping ` ({X::A. a_inv X}) \<subseteq> ({X::B. b_inv X})"
+  using inv_a_preserved by auto
 
 end