Linting ...

Give feedback for not well formed class invariants

.gitignore

@@ -2,3 +2,4 @@ output
 .afp
 *~
 *#
+Isabelle_DOF-Unit-Tests/latex_test/

.woodpecker/build.yml

@@ -1,15 +1,21 @@
 pipeline:
   build:
-    image: docker.io/logicalhacking/isabelle2022
+    image: git.logicalhacking.com/lh-docker/lh-docker-isabelle/isabelle2023:latest
+    pull: true
     commands:
+      - hg log --limit 2 /root/isabelle
+      - ./.woodpecker/check_dangling_theories
+      - ./.woodpecker/check_external_file_refs
+      - ./.woodpecker/check_quick_and_dirty
       - export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/$LATEX
       - mkdir -p $ARTIFACT_DIR
       - export `isabelle getenv ISABELLE_HOME_USER`
       - mkdir -p $ISABELLE_HOME_USER/etc
       - echo "ISABELLE_PDFLATEX=\"$LATEX --file-line-error\"" >> $ISABELLE_HOME_USER/etc/settings
-      - isabelle build -D . -o browser_info
+      - isabelle build -x HOL-Proofs -x Isabelle_DOF-Proofs -D . -o browser_info
+      - if [ "$LATEX" = "lualatex" ]; then isabelle build -o 'timeout_scale=2' -D . -o browser_info; else echo "Skipping Isabelle_DOF-Proofs for pdflatex build."; fi
+      - find . -name 'root.tex' -prune -o -name 'output' -type f | xargs latexmk -$LATEX -cd  -quiet -Werror
       - isabelle components -u .
-      - isabelle build -D . -o browser_info
       - isabelle dof_mkroot -q DOF_test
       - isabelle build -D DOF_test
       - cp -r $ISABELLE_HOME_USER/browser_info $ARTIFACT_DIR
@@ -17,7 +23,7 @@ pipeline:
       - cd ../..
       - ln -s * latest
   archive:
-    image: docker.io/logicalhacking/isabelle2022
+    image: git.logicalhacking.com/lh-docker/lh-docker-isabelle/isabelle2023:latest
     commands:
       - export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/$LATEX
       - mkdir -p $ARTIFACT_DIR
@@ -39,7 +45,7 @@ pipeline:
         from_secret: artifacts_ssh
       user: artifacts
   notify:
-    image: drillster/drone-email
+    image: docker.io/drillster/drone-email
     settings:
       host: smtp.0x5f.org
       username: woodpecker

.woodpecker/check_dangling_theories

@@ -0,0 +1,33 @@
+#!/bin/bash
+
+set -e
+
+failuremsg="Error"
+failurecode=1
+
+while [ $# -gt 0 ]
+do
+    case "$1" in
+        --warning|-w)
+            failuremsg="Warning"
+            failurecode=0;;
+    esac
+    shift
+done
+
+echo "Checking for theories that are not part of an Isabelle session:"
+echo "==============================================================="
+
+PWD=`pwd`
+TMPDIR=`mktemp -d`
+isabelle build  -D . -l -n | grep $PWD | sed -e "s| *${PWD}/||" | sort -u | grep thy$ > ${TMPDIR}/sessions-thy-files.txt
+find * -type f | sort -u | grep thy$ > ${TMPDIR}/actual-thy-files.txt
+thylist=`comm -13 ${TMPDIR}/sessions-thy-files.txt ${TMPDIR}/actual-thy-files.txt`
+if [ -z "$thylist" ] ; then
+    echo "  * Success: No dangling theories found."
+    exit 0
+else
+    echo -e "$thylist"
+    echo "$failuremsg: Dangling theories found (see list above)!" 
+    exit $failurecode 
+fi

.woodpecker/check_external_file_refs

@@ -0,0 +1,45 @@
+#!/bin/sh
+
+
+
+failuremsg="Error"
+failurecode=1
+
+while [ $# -gt 0 ]
+do
+    case "$1" in
+        --warning|-w)
+            failuremsg="Warning"
+            failurecode=0;;
+    esac
+    shift
+done
+
+DIRREGEXP="\\.\\./"
+
+echo "Checking for references pointing outside of session directory:"
+echo "=============================================================="
+
+REGEXP=$DIRREGEXP
+DIR=$DIRMATCH
+failed=0
+for i in $(seq 1 10); do 
+  FILES=`find * -mindepth $((i-1)) -maxdepth $i -type f | xargs`
+  if [ -n "$FILES" ]; then 
+    grep -s ${REGEXP} ${FILES}
+    exit=$?
+    if [ "$exit" -eq 0 ] ; then
+      failed=1
+    fi
+  fi
+  REGEXP="${DIRREGEXP}${REGEXP}"
+done
+
+
+if [ "$failed" -ne 0 ] ; then
+    echo "$failuremsg: Forbidden reference to files outside of their session directory!" 
+    exit $failurecode 
+fi
+
+echo "  * Success: No relative references to files outside of their session directory found."
+exit 0

.woodpecker/check_quick_and_dirty

@@ -0,0 +1,30 @@
+#!/bin/bash
+
+set -e
+
+failuremsg="Error"
+failurecode=1
+
+while [ $# -gt 0 ]
+do
+    case "$1" in
+        --warning|-w)
+            failuremsg="Warning"
+            failurecode=0;;
+    esac
+    shift
+done
+
+echo "Checking for sessions with quick_and_dirty mode enabled:"
+echo "========================================================"
+
+rootlist=`find -name 'ROOT' -exec grep -l 'quick_and_dirty *= *true' {} \;`
+
+if [ -z "$rootlist" ] ; then
+    echo "  * Success: No sessions with quick_and_dirty mode enabled found."
+    exit 0
+else
+    echo -e "$rootlist"
+    echo "$failuremsg: Sessions with quick_and_dirty mode enabled found (see list above)!" 
+    exit $failurecode 
+fi

.woodpecker/mk_release

@@ -83,22 +83,22 @@ build_and_install_manuals()
     if [ "$DIRTY" = "true" ]; then
         if [ -z ${ARTIFACT_DIR+x} ]; then
             echo "  * Quick and Dirty Mode (local build)"
-            $ISABELLE build -d . Isabelle_DOF-Manual 2018-cicm-isabelle_dof-applications
-            mkdir -p $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
-            cp examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/document.pdf \
-               $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
-            mkdir -p $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/
-            cp examples/technical_report/Isabelle_DOF-Manual/output/document.pdf \
-               $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/;
+            $ISABELLE build -d . Isabelle_DOF Isabelle_DOF-Example-I
+            mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF-Example-I/output/
+            cp Isabelle_DOF-Example-I/output/document.pdf \
+               $ISADOF_WORK_DIR/Isabelle_DOF-Example-I/output/
+            mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF/output/
+            cp Isabelle_DOF/output/document.pdf \
+               $ISADOF_WORK_DIR/Isabelle_DOF/output/;
         else
             echo "  * Quick and Dirty Mode (running on CI)"
-            mkdir -p $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
-            cp $ARTIFACT_DIR/browser_info/Unsorted/2018-cicm-isabelle_dof-applications/document.pdf \
-               $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
+            mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF-Example-I/output/
+            cp $ARTIFACT_DIR/browser_info/AFP/Isabelle_DOF-Example-I/document.pdf \
+               $ISADOF_WORK_DIR/Isabelle_DOF-Example-I/output/
  
-            mkdir -p $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/
-            cp $ARTIFACT_DIR/browser_info/Unsorted/Isabelle_DOF-Manual/document.pdf \
-               $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/;
+            mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF/output/
+            cp $ARTIFACT_DIR/browser_info/AFP/Isabelle_DOF/document.pdf \
+               $ISADOF_WORK_DIR/Isabelle_DOF/output/;
         fi
     else
         (cd $ISADOF_WORK_DIR && $ISABELLE env ./install-afp)
@@ -107,13 +107,13 @@ build_and_install_manuals()
     mkdir -p $ISADOF_WORK_DIR/doc
     echo "Isabelle/DOF Manuals!" > $ISADOF_WORK_DIR/doc/Contents
     
-    cp $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/document.pdf \
+    cp $ISADOF_WORK_DIR/Isabelle_DOF/output/document.pdf \
         $ISADOF_WORK_DIR/doc/Isabelle_DOF-Manual.pdf
     echo "  Isabelle_DOF-Manual                       User and Implementation Manual for Isabelle/DOF" >> $ISADOF_WORK_DIR/doc/Contents
 
-    cp $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/document.pdf \
-        $ISADOF_WORK_DIR/doc/2018-cicm-isabelle_dof-applications.pdf
-    echo "  2018-cicm-isabelle_dof-applications       Example academic paper" >> $ISADOF_WORK_DIR/doc/Contents
+    cp $ISADOF_WORK_DIR/Isabelle_DOF-Example-I/output/document.pdf \
+        $ISADOF_WORK_DIR/doc/Isabelle_DOF-Example-I.pdf
+    echo "  Isabelle_DOF-Example-I       Example academic paper" >> $ISADOF_WORK_DIR/doc/Contents
 
     find $ISADOF_WORK_DIR -type d -name "output" -exec rm -rf {} \; &> /dev/null || true
     rm -rf $ISADOF_WORK_DIR/.git* $ISADOF_WORK_DIR/.woodpecker $ISADOF_WORK_DIR/.afp 
@@ -143,7 +143,6 @@ publish_archive()
     ssh 0x5f.org chmod go+u-w -R www/$DOF_ARTIFACT_HOST/htdocs/$DOF_ARTIFACT_DIR
 }
 
-
 ISABELLE=`which isabelle`
 USE_TAG="false"
 SIGN="false"
@@ -221,4 +220,3 @@ fi
 
 rm -rf $BUILD_DIR
 
-exit 0 

CHANGELOG.md

@@ -11,7 +11,7 @@ and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.
 
 ### Changed
 
-- Updated Isabelle version to Isabelle 2022
+- Updated Isabelle version to Isabelle 2023
 
 ## [1.3.0] - 2022-07-08
 

Isabelle_DOF-Example-I/IsaDofApplications.thy

@@ -17,7 +17,7 @@ theory IsaDofApplications
 begin
 
 use_template "lncs"
-use_ontology "scholarly_paper"
+use_ontology "Isabelle_DOF.scholarly_paper"
 
 open_monitor*[this::article] 
 declare[[strict_monitor_checking=false]]
@@ -30,6 +30,61 @@ define_shortcut* isadof   \<rightleftharpoons> \<open>\isadof\<close>
 
 (* slanted text in contrast to italics *)
 define_macro* slanted_text \<rightleftharpoons> \<open>\textsl{\<close> _ \<open>}\<close>
+define_macro* unchecked_label \<rightleftharpoons> \<open>\autoref{\<close> _ \<open>}\<close>
+
+ML\<open>
+
+fun boxed_text_antiquotation name (* redefined in these more abstract terms *) =
+    DOF_lib.gen_text_antiquotation name DOF_lib.report_text 
+                           (fn ctxt => DOF_lib.string_2_text_antiquotation ctxt
+                                       #> DOF_lib.enclose_env false ctxt "isarbox")
+
+val neant = K(Latex.text("",\<^here>))
+
+fun boxed_theory_text_antiquotation name (* redefined in these more abstract terms *) =
+    DOF_lib.gen_text_antiquotation name DOF_lib.report_theory_text 
+                           (fn ctxt => DOF_lib.string_2_theory_text_antiquotation ctxt 
+                                        #> DOF_lib.enclose_env false ctxt "isarbox"
+                                        (* #> neant *)) (*debugging *)
+
+fun boxed_sml_text_antiquotation name  =
+    DOF_lib.gen_text_antiquotation name (K(K())) 
+                           (fn ctxt => Input.source_content 
+                                        #> Latex.text 
+                                        #> DOF_lib.enclose_env true ctxt "sml") 
+                           (* the simplest conversion possible *)
+
+fun boxed_pdf_antiquotation name =
+    DOF_lib.gen_text_antiquotation name (K(K())) 
+                           (fn ctxt => Input.source_content 
+                                        #> Latex.text 
+                                        #> DOF_lib.enclose_env true ctxt "out") 
+                           (* the simplest conversion possible *)
+
+fun boxed_latex_antiquotation name =
+    DOF_lib.gen_text_antiquotation name (K(K())) 
+                           (fn ctxt => Input.source_content 
+                                        #> Latex.text 
+                                        #> DOF_lib.enclose_env true ctxt "ltx") 
+                           (* the simplest conversion possible *)
+
+fun boxed_bash_antiquotation name =
+    DOF_lib.gen_text_antiquotation name (K(K())) 
+                           (fn ctxt => Input.source_content 
+                                        #> Latex.text 
+                                        #> DOF_lib.enclose_env true ctxt "bash") 
+                           (* the simplest conversion possible *)
+\<close>
+
+setup\<open>boxed_text_antiquotation         \<^binding>\<open>boxed_text\<close> #>
+      boxed_text_antiquotation         \<^binding>\<open>boxed_cartouche\<close> #>
+      boxed_theory_text_antiquotation  \<^binding>\<open>boxed_theory_text\<close> #>
+
+      boxed_sml_text_antiquotation     \<^binding>\<open>boxed_sml\<close> #>
+      boxed_pdf_antiquotation          \<^binding>\<open>boxed_pdf\<close> #>
+      boxed_latex_antiquotation        \<^binding>\<open>boxed_latex\<close>#>
+      boxed_bash_antiquotation         \<^binding>\<open>boxed_bash\<close> 
+     \<close>
 
 (*>*)
 
@@ -102,20 +157,18 @@ document evolution. Based on Isabelle infrastructures, ontologies may refer to
 types, terms, proven theorems, code, or established assertions.
 Based on a novel adaption of the Isabelle IDE, a document is checked to be 
 \<^emph>\<open>conform\<close> to a particular ontology---\<^isadof> is designed to give fast user-feedback 
-\<^emph>\<open>during the capture of content\<close>. This is particularly valuable in case of document 
+\<^emph>\<open>during the capture of content\<close>. This is particularly valuable for document 
 changes, where the \<^emph>\<open>coherence\<close> between the formal and the informal parts of the
 content can be mechanically checked.
 
-To avoid any misunderstanding: \<^isadof>  is \<^emph>\<open>not a theory in HOL\<close>   
-on ontologies and operations to track and trace links in texts,
-it is an \<^emph>\<open>environment to write structured text\<close> which \<^emph>\<open>may contain\<close>  
-\<^isabelle> definitions and proofs like mathematical articles, tech-reports and
-scientific papers---as the present one, which is written in \<^isadof> 
-itself. \<^isadof> is a plugin into the Isabelle/Isar
-framework in the style of~@{cite "wenzel.ea:building:2007"}.
+To avoid any misunderstanding: \<^isadof>  is \<^emph>\<open>not a theory in HOL\<close> on ontologies and operations 
+to track and trace links in texts, it is an \<^emph>\<open>environment to write structured text\<close> which 
+\<^emph>\<open>may contain\<close> \<^isabelle> definitions and proofs like mathematical articles, tech-reports and
+scientific papers---as the present one, which is written in \<^isadof> itself. \<^isadof> is a plugin 
+into the Isabelle/Isar framework in the style of~@{cite "wenzel.ea:building:2007"}.
 \<close>
 
-(* declaring the forward references used in the subsequent section *)  
+(* declaring the forward references used in the subsequent sections *)  
 (*<*)
 declare_reference*[bgrnd::text_section]
 declare_reference*[isadof::text_section]
@@ -123,29 +176,25 @@ declare_reference*[ontomod::text_section]
 declare_reference*[ontopide::text_section]
 declare_reference*[conclusion::text_section]
 (*>*)
-text*[plan::introduction, level="Some 1"]\<open> The plan of the paper is follows: we start by introducing  the underlying 
-Isabelle system (@{text_section (unchecked) \<open>bgrnd\<close>}) followed by presenting the 
-essentials of  \<^isadof> and its ontology language (@{text_section (unchecked) \<open>isadof\<close>}). 
+text*[plan::introduction, level="Some 1"]\<open> The plan of the paper is as follows: we start by 
+introducing the underlying Isabelle system (@{text_section (unchecked) \<open>bgrnd\<close>}) followed by 
+presenting the essentials of  \<^isadof> and its ontology language (@{text_section (unchecked) \<open>isadof\<close>}). 
 It follows @{text_section (unchecked) \<open>ontomod\<close>}, where we present three application 
 scenarios from the point of view of the ontology modeling. In @{text_section (unchecked) \<open>ontopide\<close>}
 we discuss the user-interaction generated from the ontological definitions.  Finally, we draw 
 conclusions and discuss related work in @{text_section (unchecked) \<open>conclusion\<close>}. \<close>  
 
-section*[bgrnd::text_section,main_author="Some(@{docitem ''bu''}::author)"]
+section*[bgrnd::text_section,main_author="Some(@{author ''bu''}::author)"]
         \<open> Background: The Isabelle System \<close>
 text*[background::introduction, level="Some 1"]\<open>
-While Isabelle is widely perceived as an interactive theorem prover
-for HOL (Higher-order Logic)~@{cite "nipkow.ea:isabelle:2002"}, we
-would like to emphasize the view that Isabelle is far more than that:
-it is the \<^emph>\<open>Eclipse of Formal Methods Tools\<close>.  This refers to the
-``\<^slanted_text>\<open>generic system framework of Isabelle/Isar underlying recent
-  versions of Isabelle.  Among other things, Isar provides an
-  infrastructure for Isabelle plug-ins, comprising extensible state
-  components and extensible syntax that can be bound to ML
-  programs. Thus, the Isabelle/Isar architecture may be understood as
-  an extension and refinement of the traditional `LCF approach', with
-  explicit infrastructure for building derivative
-  \<^emph>\<open>systems\<close>.\<close>''~@{cite "wenzel.ea:building:2007"} 
+While Isabelle is widely perceived as an interactive theorem prover for HOL 
+(Higher-order Logic)~@{cite "nipkow.ea:isabelle:2002"}, we would like to emphasize the view that 
+Isabelle is far more than that: it is the \<^emph>\<open>Eclipse of Formal Methods Tools\<close>.  This refers to the
+``\<^slanted_text>\<open>generic system framework of Isabelle/Isar underlying recent versions of Isabelle.  
+  Among other things, Isar provides an infrastructure for Isabelle plug-ins, comprising extensible 
+  state components and extensible syntax that can be bound to ML programs. Thus, the Isabelle/Isar 
+  architecture may be understood as an extension and refinement of the traditional `LCF approach', 
+  with explicit infrastructure for building derivative \<^emph>\<open>systems\<close>.\<close>''~@{cite "wenzel.ea:building:2007"} 
 
 The current system framework offers moreover the following features:
 
@@ -157,7 +206,7 @@ The current system framework offers moreover the following features:
   the most prominent and deeply integrated system component.
 \<close>  
 
-figure*[architecture::figure,relative_width="100",src="''figures/isabelle-architecture''"]\<open> 
+figure*[architecture::figure,relative_width="100",file_src="''figures/isabelle-architecture.pdf''"]\<open> 
      The system architecture of Isabelle (left-hand side) and the 
      asynchronous communication between the Isabelle system and 
      the IDE (right-hand side). \<close>
@@ -172,41 +221,39 @@ automated proof procedures as well as specific support for higher specification
 were built. \<close>
     
 text\<open> We would like to detail the documentation generation of the architecture,
-which is based on literate specification commands such as \inlineisar+section+ \<^dots>, 
-\inlineisar+subsection+ \<^dots>, \inlineisar+text+ \<^dots>, etc.
+which is based on literate specification commands such as \<^theory_text>\<open>section\<close> \<^dots>, 
+\<^theory_text>\<open>subsection\<close> \<^dots>, \<^theory_text>\<open>text\<close> \<^dots>, etc.
 Thus, a user can add a simple text:
-\begin{isar}
-  text\<Open>This is a description.\<Close>
-\end{isar}
+  @{boxed_theory_text [display]\<open>
+text\<open> This is a description.\<close>\<close>}
 These text-commands can be arbitrarily mixed with other commands stating definitions, proofs, code, etc.,
 and will result in the corresponding output in generated \<^LaTeX> or HTML documents. 
 Now, \<^emph>\<open>inside\<close> the textual content, it is possible to embed a \<^emph>\<open>text-antiquotation\<close>:
-\begin{isar}
-  text\<Open>According to the reflexivity axiom \at{thm refl}, we obtain in \<Gamma> 
-           for \at{term "fac 5"} the result \at{value "fac 5"}.\<Close>
-\end{isar}
+@{boxed_theory_text [display]\<open>
+   text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm refl}, 
+         we obtain in \<Gamma> for @{term "fac 5"} the result @{value "fac 5"}.\<close>\<close>}
+
 which is represented in the generated output by:
-\begin{out}
-  According to the reflexivity axiom $x = x$, we obtain in $\Gamma$ for $\operatorname{fac} 5$ the result $120$.
-\end{out}
-where \inlineisar+refl+ is actually the reference to the axiom of reflexivity in HOL. 
-For the antiquotation \inlineisar+\at{value "fac 5"}+  we assume the usual definition for 
-\inlineisar+fac+ in HOL.
+@{boxed_pdf [display]\<open>According to the reflexivity axiom $x = x$, we obtain in $\Gamma$ for $\operatorname{fac} 5$ the result $120$.\<close>}
+
+where \<^theory_text>\<open>refl\<close> is actually the reference to the axiom of reflexivity in HOL. 
+For the antiquotation \<^theory_text>\<open>@{value "''fac 5''"}\<close>  we assume the usual definition for 
+\<^theory_text>\<open>fac\<close> in HOL.
 \<close>
 
-text*[anti::introduction, level = "Some 1"]\<open> Thus, antiquotations can refer to formal content, can be type-checked before being 
-displayed and can be used for calculations before actually being typeset. When editing, 
-Isabelle's PIDE offers auto-completion and error-messages while typing the above 
-\<^emph>\<open>semi-formal\<close> content.  \<close>
+text*[anti::introduction, level = "Some 1"]\<open> Thus, antiquotations can refer to formal content, 
+can be type-checked before being displayed and can be used for calculations before actually being 
+typeset. When editing, Isabelle's PIDE offers auto-completion and error-messages while typing the 
+above \<^emph>\<open>semi-formal\<close> content.\<close>
 
-section*[isadof::technical,main_author="Some(@{docitem ''adb''}::author)"]\<open> \<^isadof> \<close>
+section*[isadof::technical,main_author="Some(@{author ''adb''}::author)"]\<open> \<^isadof> \<close>
    
 text\<open> An \<^isadof> document consists of three components: 
 \<^item> the \<^emph>\<open>ontology definition\<close> which is an Isabelle theory file with definitions
   for document-classes and all auxiliary datatypes.  
 \<^item> the \<^emph>\<open>core\<close> of the document itself which is an Isabelle theory
   importing the ontology definition. \<^isadof> provides an own family of text-element
-  commands such as \inlineisar+title*+, \inlineisar+section*+,  \inlineisar+text*+, etc., 
+  commands such as \<^theory_text>\<open>title*\<close>, \<^theory_text>\<open>section*\<close>, \<^theory_text>\<open>text*\<close>, etc., 
   which can be annotated with meta-information defined in the underlying  ontology definition.
 \<^item> the \<^emph>\<open>layout definition\<close> for the given ontology exploiting this meta-information.
 \<close>
@@ -215,7 +262,7 @@ three parts. Note that the document core \<^emph>\<open>may\<close>, but \<^emph
 use Isabelle definitions or proofs for checking the formal content---the 
 present paper is actually an example of a document not containing any proof.
 
- The document generation process of \<^isadof> is currently restricted to \LaTeX, which means
+ The document generation process of \<^isadof> is currently restricted to \<^LaTeX>, which means
 that the layout is defined by a set of \<^LaTeX> style files. Several layout 
 definitions for one ontology are possible and pave the way that different \<^emph>\<open>views\<close> for
 the same central document were generated, addressing the needs of different purposes `
@@ -229,65 +276,47 @@ style-files (\<^verbatim>\<open>.sty\<close>-files). In the document core author
 their source, but this limits the possibility of using different representation technologies, 
 \<^eg>, HTML, and increases the risk of arcane error-messages in generated \<^LaTeX>. 
 
- The \<^isadof> ontology specification language consists basically on a notation for
-document classes, where the attributes were typed with HOL-types and can be instantiated 
-by terms HOL-terms, \<^ie>, the actual parsers and type-checkers of the Isabelle system were reused.
-This has the particular advantage that \<^isadof> commands can be arbitrarily mixed with 
-Isabelle/HOL commands providing the machinery for type declarations and term specifications such
-as enumerations. In particular, document class definitions provide:
+The \<^isadof> ontology specification language consists basically on a notation for document classes, 
+where the attributes were typed with HOL-types and can be instantiated by terms HOL-terms, \<^ie>, 
+the actual parsers and type-checkers of the Isabelle system were reused. This has the particular 
+advantage that \<^isadof> commands can be arbitrarily mixed with Isabelle/HOL commands providing the 
+machinery for type declarations and term specifications such as enumerations. In particular, 
+document class definitions provide:
 \<^item>  a HOL-type for each document class as well as inheritance, 
 \<^item>  support for attributes with HOL-types and optional default values,
 \<^item>  support for overriding of attribute defaults but not overloading, and
 \<^item>  text-elements annotated with document classes; they are mutable 
-   instances of document classes.
-\<close>
+   instances of document classes.\<close>
+
 text\<open>
-Attributes referring to other ontological concepts are called \<^emph>\<open>links\<close>.
-The HOL-types inside the document specification language support built-in types for Isabelle/HOL 
-\inlineisar+typ+'s,  \inlineisar+term+'s, and \inlineisar+thm+'s reflecting internal Isabelle's 
-internal types  for these entities; when denoted in HOL-terms to instantiate an attribute, for 
-example, there is a  specific syntax (called \<^emph>\<open>inner syntax antiquotations\<close>) that is checked by 
-\<^isadof> for consistency.
+Attributes referring to other ontological concepts are called \<^emph>\<open>links\<close>. The HOL-types inside the 
+document specification language support built-in types for Isabelle/HOL \<^theory_text>\<open>typ\<close>'s, \<^theory_text>\<open>term\<close>'s, and
+\<^theory_text>\<open>thm\<close>'s reflecting internal Isabelle's internal types  for these entities; when denoted in 
+HOL-terms  to instantiate an attribute, for example, there is a  specific syntax 
+(called \<^emph>\<open>inner syntax antiquotations\<close>) that is checked by \<^isadof> for consistency.
 
-Document classes can have a \inlineisar+where+ clause containing a regular 
-expression over class names. Classes with such a \inlineisar+where+ were called \<^emph>\<open>monitor classes\<close>.
-While document classes and their inheritance relation structure meta-data of text-elements
-in an object-oriented manner, monitor classes enforce structural organization
-of documents via the language specified by the regular expression 
-enforcing a sequence of text-elements that must belong to the corresponding classes. 
-
-To start using \<^isadof>, one creates an Isabelle project (with the name 
-\inlinebash{IsaDofApplications}):
-\begin{bash}
-  isabelle dof_mkroot -o scholarly_paper -t lncs IsaDofApplications
-\end{bash}
-where the \inlinebash{-o scholarly_paper} specifies the ontology for writing scientific articles and 
-\inlinebash{-t lncs} specifies the use of Springer's \LaTeX-configuration for the Lecture Notes in 
-Computer Science series. The project can be formally checked, including the generation of the 
-article in PDF using the  following command:
-\begin{bash}
-  isabelle build -d . IsaDofApplications
-\end{bash}
-\<close>
+Document classes can have a \<^theory_text>\<open>where\<close> clause containing a regular expression over class names. 
+Classes with such a \<^theory_text>\<open>where\<close>  were called \<^emph>\<open>monitor classes\<close>. While document classes and their 
+inheritance relation structure meta-data of text-elements in an object-oriented manner, monitor 
+classes enforce structural organization of documents via the language specified by the regular 
+expression enforcing a sequence of text-elements that belong to the corresponding classes.  \<^vs>\<open>-0.4cm\<close>\<close>
 
 section*[ontomod::text_section]\<open> Modeling Ontologies in \<^isadof> \<close> 
-text\<open> In this section, we will use the \<^isadof> document ontology language
-for three different application scenarios: for scholarly papers, for mathematical 
-exam sheets as well as standardization documents where the concepts of the
-standard are captured in the ontology. For space reasons, we will concentrate in all three
-cases on aspects of the modeling due to space limitations.\<close>
+text\<open> In this section, we will use the \<^isadof> document ontology language for three different 
+application scenarios: for scholarly papers, for mathematical exam sheets as well as standardization 
+documents where the concepts of the standard are captured in the ontology. For space reasons, we 
+will concentrate in all three cases on aspects of the modeling due to space limitations.\<close>
 
 subsection*[scholar_onto::example]\<open> The Scholar Paper Scenario: Eating One's Own Dog Food. \<close>  
 text\<open> The following ontology is a simple ontology modeling scientific papers. In this 
 \<^isadof> application scenario, we deliberately refrain from integrating references to
 (Isabelle) formal content in order  demonstrate that \<^isadof> is not a framework from 
-Isabelle users to Isabelle users only.
-Of course, such references can be added easily and represent a particular strength  
-of \<^isadof>.
+Isabelle users to Isabelle users only. Of course, such references can be added easily and 
+represent a particular strength of \<^isadof>.\<close>
 
-
-\begin{figure}
-\begin{isar}
+text*["paper_onto_core"::float, 
+      main_caption="\<open>The core of the ontology definition for writing scholarly papers.\<close>"]
+\<open>@{boxed_theory_text [display]\<open>
 doc_class title =
    short_title :: "string option"  <=  None
      
@@ -302,64 +331,62 @@ doc_class abstract =
 
 doc_class text_section = 
    main_author :: "author option"  <=  None
-   todo_list   :: "string list"    <=  "[]"
-\end{isar}
-\caption{The core of the ontology definition for writing scholarly papers.}
-\label{fig:paper-onto-core}
-\end{figure}
-The first part of the ontology \inlineisar+scholarly_paper+ (see \autoref{fig:paper-onto-core})
+   todo_list   :: "string list"    <=  "[]" 
+\<close>}\<close>
+
+text\<open> The first part of the ontology \<^theory_text>\<open>scholarly_paper\<close> 
+(see @{float "paper_onto_core"})
 contains the document class definitions
-with the usual text-elements of a scientific paper. The attributes \inlineisar+short_title+, 
-\inlineisar+abbrev+ etc are introduced with their types as well as their default values.
-Our model prescribes an optional \inlineisar+main_author+ and a todo-list attached to an arbitrary 
+with the usual text-elements of a scientific paper. The attributes \<^theory_text>\<open>short_title\<close>, 
+\<^theory_text>\<open>abbrev\<close> etc are introduced with their types as well as their default values.
+Our model prescribes an optional \<^theory_text>\<open>main_author\<close> and a todo-list attached to an arbitrary 
 text section; since instances of this class are mutable (meta)-objects of text-elements, they
 can be modified arbitrarily through subsequent text and of course globally during text evolution.
-Since \inlineisar+author+ is a HOL-type internally generated by \<^isadof> framework and can therefore
-appear in the \inlineisar+main_author+ attribute of the \inlineisar+text_section+ class; 
+Since \<^theory_text>\<open>author\<close> is a HOL-type internally generated by \<^isadof> framework and can therefore
+appear in the \<^theory_text>\<open>main_author\<close> attribute  of the \<^theory_text>\<open>text_section\<close> class; 
 semantic links between concepts can be modeled this way.
 
 The translation of its content to, \<^eg>, Springer's \<^LaTeX> setup for the Lecture Notes in Computer 
-Science Series, as required by many scientific conferences, is mostly straight-forward. \<close>
+Science Series, as required by many scientific conferences, is mostly straight-forward. 
+\<^vs>\<open>-0.8cm\<close>\<close>
 
-figure*[fig1::figure,spawn_columns=False,relative_width="95",src="''figures/Dogfood-Intro''"]
+figure*[fig1::figure,relative_width="95",file_src="''figures/Dogfood-Intro.png''"]
        \<open> Ouroboros I: This paper from inside \<^dots> \<close>  
 
-text\<open> @{figure \<open>fig1\<close>} shows the corresponding view in the Isabelle/PIDE of thqqe present paper.
+(*<*)declare_reference*[paper_onto_sections::float](*>*)
+text\<open>\<^vs>\<open>-0.8cm\<close> @{figure \<open>fig1\<close>} shows the corresponding view in the Isabelle/PIDE of the present paper.
 Note that the text uses \<^isadof>'s own text-commands containing the meta-information provided by
 the underlying ontology.
-We proceed by a definition of \inlineisar+introduction+'s, which we define as the extension of
-\inlineisar+text_section+ which is intended to capture common infrastructure:
-\begin{isar}
+We proceed by a definition of \<^theory_text>\<open>introduction\<close>'s, which we define as the extension of
+\<^theory_text>\<open>text_section\<close> which is intended to capture common infrastructure:
+@{boxed_theory_text [display]\<open>
 doc_class introduction = text_section +
    comment :: string
-\end{isar}
-As a consequence of the definition as extension, the \inlineisar+introduction+ class
-inherits the attributes \inlineisar+main_author+ and \inlineisar+todo_list+ together with 
+\<close>}
+As a consequence of the definition as extension, the \<^theory_text>\<open>introduction\<close> class
+inherits the attributes \<^theory_text>\<open>main_author\<close> and \<^theory_text>\<open>todo_list\<close> together with 
 the corresponding default values.
 
 As a variant of the introduction, we could add here an attribute that contains the formal 
 claims of the article --- either here, or, for example, in the keyword list of the abstract. 
-As type, one could use either the built-in type \inlineisar+term+ (for syntactically correct, 
-but not necessarily proven entity) or \inlineisar+thm+ (for formally proven entities). It suffices 
+As type, one could use either the built-in type \<^theory_text>\<open>term\<close> (for syntactically correct, 
+but not necessarily proven entity) or \<^theory_text>\<open>thm\<close> (for formally proven entities). It suffices 
 to add the line:
-\begin{isar}
+@{boxed_theory_text [display]\<open>
    claims  :: "thm list"
-\end{isar}
-and to extent the \LaTeX-style accordingly to handle the additional field. 
-Note that \inlineisar+term+ and \inlineisar+thm+ are types reflecting the core-types of the
+\<close>}
+and to extent the \<^LaTeX>-style accordingly to handle the additional field. 
+Note that \<^theory_text>\<open>term\<close> and \<^theory_text>\<open>thm\<close> are types reflecting the core-types of the
 Isabelle kernel. In a corresponding conclusion section, one could model analogously an 
 achievement section; by programming a specific compliance check in SML, the implementation 
 of automated forms of validation check for specific categories of papers is envisageable. 
 Since this requires deeper knowledge in Isabelle programming, however, we consider this out 
 of the scope of this paper.
 
-
-We proceed more or less conventionally by the subsequent sections (\autoref{fig:paper-onto-sections})
-\begin{figure}
-\begin{isar}
-doc_class technical = text_section +
-   definition_list :: "string list" <=  "[]"
-
+We proceed more or less conventionally by the subsequent sections (@{float (unchecked)\<open>paper_onto_sections\<close>})\<close>  
+text*["paper_onto_sections"::float, 
+      main_caption = "''Various types of sections of a scholarly papers.''"]\<open>
+@{boxed_theory_text [display]\<open>
 doc_class example   = text_section +
    comment :: string
 
@@ -371,14 +398,13 @@ doc_class related_work = conclusion +
 
 doc_class bibliography =
    style :: "string option"  <=  "''LNCS''"
-\end{isar}
-\caption{Various types of sections of a scholarly papers.}
-\label{fig:paper-onto-sections}
-\end{figure}
- and finish with a monitor class definition that enforces a textual ordering
-in the document core by a regular expression (\autoref{fig:paper-onto-monitor}).
-\begin{figure}
-\begin{isar}
+\<close>}\<close>
+(*<*)declare_reference*[paper_onto_monitor::float](*>*)
+text\<open>... and finish with a monitor class definition that enforces a textual ordering
+in the document core by a regular expression (@{float (unchecked) "paper_onto_monitor"}).\<close>  
+text*["paper_onto_monitor"::float, 
+      main_caption = "''A monitor for the scholarly paper ontology.''"]\<open>
+@{boxed_theory_text [display]\<open>
 doc_class article = 
    trace :: "(title + subtitle + author+ abstract +
               introduction + technical + example +
@@ -386,23 +412,20 @@ doc_class article =
    where "(title       ~~ \<lbrakk>subtitle\<rbrakk>   ~~ \<lbrace>author\<rbrace>$^+$+  ~~  abstract    ~~
              introduction ~~  \<lbrace>technical || example\<rbrace>$^+$  ~~  conclusion ~~  
              bibliography)"
-\end{isar}
-\caption{A monitor for the scholarly paper ontology.}
-\label{fig:paper-onto-monitor}
-\end{figure}
+\<close>}
 \<close>
 text\<open> We might wish to add a component into our ontology that models figures to be included into 
 the document. This boils down to the exercise of modeling structured data in the style of a 
 functional programming language in HOL and to reuse the implicit HOL-type inside a suitable document 
-class \inlineisar+figure+:
-\begin{isar}
+class \<^theory_text>\<open>figure\<close>:
+@{boxed_theory_text [display]\<open>
 datatype placement = h | t | b | ht | hb   
 doc_class figure   = text_section +
    relative_width   :: "int" (* percent of textwidth *)    
    src     :: "string"
    placement :: placement 
    spawn_columns :: bool <= True 
-\end{isar}
+\<close>}
 \<close>
 
 text\<open> Alternatively, by including the HOL-libraries for rationals, it is possible to 
@@ -410,11 +433,11 @@ use fractions or even mathematical reals. This must be counterbalanced by syntac
 and semantic convenience. Choosing the mathematical reals, \<^eg>, would have the drawback that 
 attribute evaluation could be substantially more complicated.\<close>
 
-figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figures/Dogfood-figures''"]
+figure*[fig_figures::figure,relative_width="85",file_src="''figures/Dogfood-figures.png''"]
        \<open> Ouroboros II: figures \<^dots> \<close>
 
-text\<open> The document class \inlineisar+figure+ --- supported by the \<^isadof> text command 
-\inlineisar+figure*+ --- makes it possible to express the pictures and diagrams in this paper 
+text\<open> The document class \<^theory_text>\<open>figure\<close> --- supported by the \<^isadof> text command 
+\<^theory_text>\<open>figure*\<close> --- makes it possible to express the pictures and diagrams in this paper 
 such as @{figure \<open>fig_figures\<close>}.
 \<close>
          
@@ -437,10 +460,10 @@ We assume that the content has four different types of addressees, which have a
 text\<open> The latter quality assurance mechanism is used in many universities,
 where for organizational reasons the execution of an exam takes place in facilities
 where the author of the exam is not expected to be physically present.
-Furthermore, we assume a simple grade system (thus, some calculation is required). 
-
-\begin{figure}
-\begin{isar}
+Furthermore, we assume a simple grade system (thus, some calculation is required). \<close>  
+text*["onto_exam"::float, 
+      main_caption = "''The core of the ontology modeling math exams.''"]\<open>
+@{boxed_theory_text [display]\<open>
 doc_class Author = ...
 datatype Subject =  algebra | geometry | statistical
 datatype Grade =  A1 | A2 | A3
@@ -462,18 +485,18 @@ doc_class Exam_item =
   concerns :: "ContentClass set"  
 
 type_synonym SubQuestion = string
-\end{isar}
-\caption{The core of the ontology modeling math exams.}
-\label{fig:onto-exam}
-\end{figure}
-The heart of this ontology (see \autoref{fig:onto-exam}) is an alternation of questions and answers, 
+\<close>}\<close>
+
+(*<*)declare_reference*[onto_questions::float](*>*)
+text\<open>The heart of this ontology (see @{float "onto_exam"}) is an alternation of questions and answers, 
 where the answers can consist of simple yes-no answers (QCM style check-boxes) or lists of formulas. 
 Since we do not
-assume familiarity of the students with Isabelle (\inlineisar+term+ would assume that this is a 
+assume familiarity of the students with Isabelle (\<^theory_text>\<open>term\<close> would assume that this is a 
 parse-able and type-checkable entity), we basically model a derivation as a sequence of strings
-(see \autoref{fig:onto-questions}).
-\begin{figure}
-\begin{isar}
+(see @{float (unchecked)"onto_questions"}).\<close>  
+text*["onto_questions"::float, 
+      main_caption = "''An exam can contain different types of questions.''"]\<open>
+@{boxed_theory_text [display]\<open>
 doc_class Answer_Formal_Step =  Exam_item +
   justification :: string
   "term"        :: "string" 
@@ -497,19 +520,18 @@ doc_class Exercise = Exam_item +
   content  :: "(Task) list"
   concerns :: "ContentClass set" <= "UNIV" 
   mark     :: int
-\end{isar}
-\caption{An exam can contain different types of questions.}
-\label{fig:onto-questions}
-\end{figure}
-
+\<close>}\<close>
+(*<*)declare_reference*[onto_exam_monitor::float](*>*)
+text\<open>
 In many institutions, it makes sense to have a rigorous process of validation
 for exam subjects: is the initial question correct? Is a proof in the sense of the
 question possible? We model the possibility that the @{term examiner} validates a 
-question by a sample proof validated by Isabelle (see \autoref{fig:onto-exam-monitor}). 
+question by a sample proof validated by Isabelle (see @{float (unchecked) "onto_exam_monitor"}). 
 In our scenario this sample proofs are completely \<^emph>\<open>intern\<close>, \<^ie>, not exposed to the 
-students but just additional material for the internal review process of the exam.
-\begin{figure}
-\begin{isar}
+students but just additional material for the internal review process of the exam.\<close>  
+text*["onto_exam_monitor"::float, 
+      main_caption = "''Validating exams.''"]\<open>
+@{boxed_theory_text [display]\<open>
 doc_class Validation = 
    tests  :: "term list"  <="[]"
    proofs :: "thm list"   <="[]"
@@ -523,14 +545,9 @@ doc_class MathExam=
   content :: "(Header + Author + Exercise) list"
   global_grade :: Grade 
   where "\<lbrace>Author\<rbrace>$^+$  ~~  Header ~~  \<lbrace>Exercise ~~ Solution\<rbrace>$^+$ "
-\end{isar}
-\caption{Validating exams.}
-\label{fig:onto-exam-monitor}
-\end{figure}
-\<close>
-
+\<close>}\<close>
   
-declare_reference*["fig_qcm"::figure]
+(*<*)declare_reference*["fig_qcm"::figure](*>*)
 
 text\<open> Using the \<^LaTeX> package hyperref, it is possible to conceive an interactive 
 exam-sheets with multiple-choice and/or free-response elements 
@@ -538,14 +555,14 @@ exam-sheets with multiple-choice and/or free-response elements
 help of the latter, it is possible that students write in a browser a formal mathematical 
 derivation---as part of an algebra exercise, for example---which is submitted to the examiners 
 electronically. \<close>
-figure*[fig_qcm::figure,spawn_columns=False,
-        relative_width="90",src="''figures/InteractiveMathSheet''"]
-        \<open> A Generated QCM Fragment \<^dots> \<close>  
+figure*[fig_qcm::figure,
+        relative_width="90",file_src="''figures/InteractiveMathSheet.png''"]
+        \<open>A Generated QCM Fragment \<^dots> \<close>  
 
 subsection*[cenelec_onto::example]\<open> The Certification Scenario following CENELEC \<close>
 text\<open> Documents to be provided in formal certifications (such as CENELEC
-50126/50128, the DO-178B/C, or Common Criteria) can much profit from the control of ontological consistency: 
-a lot of an evaluators work consists in tracing down the links from requirements over 
+50126/50128, the DO-178B/C, or Common Criteria) can much profit from the control of ontological 
+consistency: a lot of an evaluators work consists in tracing down the links from requirements over 
 assumptions down to elements of evidence, be it in the models, the code, or the tests. 
 In a certification process, traceability becomes a major concern; and providing
 mechanisms to ensure complete traceability already at the development of the
@@ -557,15 +574,17 @@ of developments targeting certifications. Continuously checking the links betwee
 and the semi-formal parts of such documents is particularly valuable during the (usually
 collaborative) development effort. 
 
-As in many other cases, formal certification documents come with an own terminology and
-pragmatics of what has to be demonstrated and where, and how the trace-ability of requirements through
+As in many other cases, formal certification documents come with an own terminology and pragmatics 
+of what has to be demonstrated and where, and how the trace-ability of requirements through
 design-models over code to system environment assumptions has to be assured.  
 \<close>
+(*<*)declare_reference*["conceptual"::float](*>*)
 text\<open> In the sequel, we present a simplified version of an ontological model used in a 
 case-study~ @{cite "bezzecchi.ea:making:2018"}. We start with an introduction of the concept of requirement 
-(see \autoref{fig:conceptual}). 
-\begin{figure}
-\begin{isar}
+(see @{float (unchecked) "conceptual"}). \<close>  
+text*["conceptual"::float, 
+      main_caption = "''Modeling requirements.''"]\<open>
+@{boxed_theory_text [display]\<open>
 doc_class requirement = long_name :: "string option"
 
 doc_class requirement_analysis = no :: "nat"
@@ -578,11 +597,9 @@ datatype ass_kind = informal | semiformal | formal
   
 doc_class assumption = requirement +
      assumption_kind :: ass_kind <= informal 
-\end{isar}
-\caption{Modeling requirements.}
-\label{fig:conceptual}
-\end{figure}
-Such ontologies can be enriched by larger explanations and examples, which may help
+\<close>}\<close>
+
+text\<open>Such ontologies can be enriched by larger explanations and examples, which may help
 the team of engineers substantially when developing the central document for a certification, 
 like an explication what is precisely the difference between an \<^emph>\<open>hypothesis\<close> and an 
 \<^emph>\<open>assumption\<close> in the context of the evaluation standard. Since the PIDE makes for each 
@@ -604,71 +621,70 @@ is the category \<^emph>\<open>safety related application condition\<close> (or
 for short) which is used for \<^emph>\<open>ec\<close>'s that establish safety properties
 of the evaluation target. Their track-ability throughout the certification
 is therefore particularly critical. This is naturally modeled as follows:
-\begin{isar}  
+@{boxed_theory_text [display]\<open>  
 doc_class ec = assumption  +
      assumption_kind :: ass_kind <= (*default *) formal
                         
 doc_class srac = ec  +
      assumption_kind :: ass_kind <= (*default *) formal
-\end{isar}
+\<close>}
 \<close>
    
 section*[ontopide::technical]\<open> Ontology-based IDE support \<close>  
 text\<open> We present a selection of interaction scenarios  @{example \<open>scholar_onto\<close>}
 and @{example \<open>cenelec_onto\<close>} with Isabelle/PIDE instrumented by \<^isadof>. \<close>
 
+(*<*)
+declare_reference*["text_elements"::float]
+declare_reference*["hyperlinks"::float]
+(*>*)
+
 subsection*[scholar_pide::example]\<open> A Scholarly Paper \<close>  
-text\<open> In \autoref{fig-Dogfood-II-bgnd1} and \autoref{fig-bgnd-text_section} we show how
+text\<open> In @{float (unchecked) "text_elements"}~(a)
+and @{float (unchecked) "text_elements"}~(b)we show how
 hovering over links permits to explore its meta-information. 
 Clicking on a document class identifier permits to hyperlink into the corresponding
-class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an attribute-definition
-(which is qualified in order to disambiguate; \autoref{fig:Dogfood-V-attribute}).
+class definition (@{float (unchecked) "hyperlinks"}~(a)); hovering over an attribute-definition
+(which is qualified in order to disambiguate; @{float (unchecked) "hyperlinks"}~(b)).
 \<close>
-     
-side_by_side_figure*["text-elements"::side_by_side_figure,anchor="''fig-Dogfood-II-bgnd1''",
-                      caption="''Exploring a Reference of a Text-Element.''",relative_width="48",
-                      src="''figures/Dogfood-II-bgnd1''",anchor2="''fig-bgnd-text_section''",
-                      caption2="''Exploring the class of a text element.''",relative_width2="47",
-                      src2="''figures/Dogfood-III-bgnd-text_section''"]\<open> Exploring text elements. \<close>
 
-side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-jumpInDocCLass''",
-                      caption="''Hyperlink to Class-Definition.''",relative_width="48",
-                      src="''figures/Dogfood-IV-jumpInDocCLass''",anchor2="''fig:Dogfood-V-attribute''",
-                      caption2="''Exploring an attribute.''",relative_width2="47",
-                      src2="''figures/Dogfood-III-bgnd-text_section''"]\<open> Hyperlinks.\<close>
+text*["text_elements"::float, 
+      main_caption="\<open>Exploring text elements.\<close>"]
+\<open>
+@{fig_content (width=53, height=5, caption="Exploring a reference of a text element.") "figures/Dogfood-II-bgnd1.png"
+}\<^hfill>@{fig_content (width=47, height=5, caption="Exploring the class of a text element.") "figures/Dogfood-III-bgnd-text_section.png"} 
+\<close>
 
+text*["hyperlinks"::float, 
+      main_caption="\<open>Hyperlinks.\<close>"]
+\<open>
+@{fig_content (width=48, caption="Hyperlink to Class-Definition.") "figures/Dogfood-IV-jumpInDocCLass.png"
+}\<^hfill>@{fig_content (width=47, caption="Exploring an attribute.") "figures/Dogfood-V-attribute.png"} 
+\<close>
 
-declare_reference*["figDogfoodVIlinkappl"::figure]
-text\<open> An ontological reference application in \autoref{figDogfoodVIlinkappl}: the ontology-dependant 
-antiquotation \inlineisar|@ {example ...}| refers to the corresponding text-elements. Hovering allows 
-for inspection, clicking for jumping to the definition.  If the link does not exist or has a 
-non-compatible type, the text is not validated.  \<close>
-
-figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-V-attribute''"]
-       \<open> Exploring an attribute (hyperlinked to the class). \<close> 
 subsection*[cenelec_pide::example]\<open> CENELEC  \<close>
-declare_reference*[figfig3::figure]  
-text\<open> The corresponding view in @{docitem (unchecked) \<open>figfig3\<close>} shows core part of a document,  
+(*<*)declare_reference*[figfig3::figure](*>*)  
+text\<open> The corresponding view in @{figure (unchecked) \<open>figfig3\<close>} shows core part of a document,  
 coherent to the @{example \<open>cenelec_onto\<close>}. The first sample shows standard Isabelle antiquotations 
 @{cite "wenzel:isabelle-isar:2017"} into formal entities of a theory. This way, the informal parts 
 of a document get ``formal content'' and become more robust under change.\<close>
 
-figure*[figfig3::figure,relative_width="80",src="''figures/antiquotations-PIDE''"]
+figure*[figfig3::figure,relative_width="80",file_src="''figures/antiquotations-PIDE.png''"]
 \<open> Standard antiquotations referring to theory elements.\<close>
 
-declare_reference*[figfig5::figure]  
+(*<*)declare_reference*[figfig5::figure]  (*>*)
 text\<open> The subsequent sample in @{figure (unchecked) \<open>figfig5\<close>} shows the definition of an 
 \<^emph>\<open>safety-related application condition\<close>, a side-condition of a theorem which 
 has the consequence that a certain calculation must be executed sufficiently fast on an embedded 
 device. This condition can not be established inside the formal theory but has to be 
 checked by system integration tests.\<close>
   
-figure*[figfig5::figure, relative_width="80", src="''figures/srac-definition''"]
+figure*[figfig5::figure, relative_width="80", file_src="''figures/srac-definition.png''"]
         \<open> Defining a SRAC reference \<^dots> \<close>
-figure*[figfig7::figure, relative_width="80", src="''figures/srac-as-es-application''"]
+figure*[figfig7::figure, relative_width="80", file_src="''figures/srac-as-es-application.png''"]
         \<open> Using a SRAC as EC document reference. \<close>
        
-text\<open> Now we reference in @{figure (unchecked) \<open>figfig7\<close>} this safety-related condition; 
+text\<open> Now we reference in @{figure \<open>figfig7\<close>} this safety-related condition; 
 however, this happens in a context where general \<^emph>\<open>exported constraints\<close> are listed. 
 \<^isadof>'s checks establish that this is legal in the given ontology. 
 
@@ -680,7 +696,7 @@ informal parts. \<close>
 section*[onto_future::technical]\<open> Monitor Classes \<close>  
 text\<open> Besides sub-typing, there is another relation between
 document classes: a class can be a \<^emph>\<open>monitor\<close> to other ones,
-which is expressed by the occurrence of a \inlineisar+where+ clause
+which is expressed by the occurrence of a @{theory_text \<open>where\<close>} clause
 in the document class definition containing a regular
 expression (see @{example \<open>scholar_onto\<close>}).
 While class-extension refers to data-inheritance of attributes,
@@ -689,8 +705,8 @@ in which instances of monitored classes may occur. \<close>
 
 text\<open>
 The control of monitors is done by the commands:
-\<^item> \inlineisar+open_monitor* +  <doc-class>
-\<^item> \inlineisar+close_monitor* + <doc-class> 
+\<^item> \<^theory_text>\<open>open_monitor*\<close> \<^emph>\<open><doc-class>\<close>  
+\<^item> \<^theory_text>\<open>close_monitor*\<close> \<^emph>\<open><doc-class>\<close> 
 \<close>
 text\<open>
 where the automaton of the monitor class is expected to be in a final state. In the final state, 
@@ -738,8 +754,7 @@ work in this area we are aware of is rOntorium~@{cite "rontorium"}, a plugin
 for \<^Protege> that integrates R~@{cite "adler:r:2010"} into an
 ontology environment. Here, the main motivation behind this
 integration is to allow for statistically analyze ontological
-documents. Thus, this is complementary to our work.
-\<close>
+documents. Thus, this is complementary to our work.\<close>
 
 text\<open> \<^isadof> in its present form has a number of technical short-comings as well 
   as potentials not yet explored. On the long list of the short-comings is the 

Isabelle_DOF-Example-I/ROOT

@@ -1,13 +1,14 @@
-session "2018-cicm-isabelle_dof-applications" = "Isabelle_DOF" + 
-  options [document = pdf, document_output = "output", document_build = dof, quick_and_dirty = true]
+chapter AFP
+
+session "Isabelle_DOF-Example-I" (AFP) = "Isabelle_DOF" + 
+  options [document = pdf, document_output = "output", document_build = dof, timeout = 300]
   theories
     IsaDofApplications
   document_files
     "root.bib"
     "authorarchive.sty"
     "preamble.tex"
-    "lstisadof.sty"
-    "vector_iD_icon.pdf"
+    "lstisadof-manual.sty"
     "figures/isabelle-architecture.pdf"
     "figures/Dogfood-Intro.png"
     "figures/InteractiveMathSheet.png"

Isabelle_DOF-Example-I/document/authorarchive.sty

@@ -1,4 +1,4 @@
-%% Copyright (C) 2008-2019 Achim D. Brucker, https://www.brucker.ch
+%% Copyright (C) 2008-2023 Achim D. Brucker, https://www.brucker.ch
 %%
 %% License:
 %%   This program can be redistributed and/or modified under the terms
@@ -11,21 +11,22 @@
 %%   SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
 \NeedsTeXFormat{LaTeX2e}\relax
 \ProvidesPackage{authorarchive}
-  [0000/00/00 Unreleased v1.1.1+%
+  [2023/02/10 v1.3.0
   Self-archiving information for scientific publications.]
 %
 \PassOptionsToPackage{hyphens}{url}
 %
 \RequirePackage{ifthen}
 \RequirePackage[inline]{enumitem}
-\RequirePackage{graphicx}
+\RequirePackage{orcidlink}
 \RequirePackage{eso-pic}
 \RequirePackage{intopdf}
 \RequirePackage{kvoptions}
 \RequirePackage{hyperref}
 \RequirePackage{calc}
 \RequirePackage{qrcode}
-\RequirePackage{hvlogos}
+\RequirePackage{etoolbox}
+\newrobustcmd\BibTeX{Bib\TeX}
 %
 %Better url breaking
 \g@addto@macro{\UrlBreaks}{\UrlOrds}
@@ -80,31 +81,51 @@
 }
 \ProcessKeyvalOptions*
 
-% Provide command for dynamic configuration seutp
-\def\authorsetup{\kvsetkeys{AA}}
+\newcommand{\AA@defIncludeFiles}{
+  \def\AA@bibBibTeX{\AA@bibtexdir/\AA@key.bib}
+  \def\AA@bibBibTeXLong{\AA@bibtexdir/\AA@key.bibtex}
+  \def\AA@bibWord{\AA@bibtexdir/\AA@key.word.xml}
+  \def\AA@bibEndnote{\AA@bibtexdir/\AA@key.enw}
+  \def\AA@bibRIS{\AA@bibtexdir/\AA@key.ris}
+}
+\AA@defIncludeFiles
+
+\newboolean{AA@bibExists}
+\setboolean{AA@bibExists}{false}
+\newcommand{\AA@defIncludeSwitches}{
+  \IfFileExists{\AA@bibBibTeX}{\setboolean{AA@bibExists}{true}}{}
+  \IfFileExists{\AA@bibBibTeXLong}{\setboolean{AA@bibExists}{true}}{}
+  \IfFileExists{\AA@bibWord}{\setboolean{AA@bibExists}{true}}{}
+  \IfFileExists{\AA@bibEndnote}{\setboolean{AA@bibExists}{true}}{}
+  \IfFileExists{\AA@bibRIS}{\setboolean{AA@bibExists}{true}}{}
+}
+\AA@defIncludeSwitches
+
+
+% Provide command for dynamic configuration setup
+% \def\authorsetup{\kvsetkeys{AA}}
+\newcommand{\authorsetup}[1]{%
+  \kvsetkeys{AA}{#1}
+  \AA@defIncludeFiles
+  \AA@defIncludeSwitches
+}
 
 % Load local configuration
 \InputIfFileExists{authorarchive.config}{}{}
 
+%  define proxy command for setting PDF attributes
+\ExplSyntaxOn
+\@ifundefined{pdfmanagement_add:nnn}{%
+    \newcommand{\AA@pdfpagesattribute}[2]{\pdfpagesattr{/#1 #2}}%
+ }{%
+    \newcommand{\AA@pdfpagesattribute}[2]{\pdfmanagement_add:nnn{Pages}{#1}{#2}}%
+ }%
+\ExplSyntaxOff
 
 \newlength\AA@x
 \newlength\AA@y
 \newlength\AA@width
 
-\def\AA@bibBibTeX{\AA@bibtexdir/\AA@key.bib}
-\def\AA@bibBibTeXLong{\AA@bibtexdir/\AA@key.bibtex}
-\def\AA@bibWord{\AA@bibtexdir/\AA@key.word.xml}
-\def\AA@bibEndnote{\AA@bibtexdir/\AA@key.enw}
-\def\AA@bibRIS{\AA@bibtexdir/\AA@key.ris}
-
-\newboolean{AA@bibExists}
-\setboolean{AA@bibExists}{false}
-\IfFileExists{\AA@bibBibTeX}{\setboolean{AA@bibExists}{true}}{}
-\IfFileExists{\AA@bibBibTeXLong}{\setboolean{AA@bibExists}{true}}{}
-\IfFileExists{\AA@bibWord}{\setboolean{AA@bibExists}{true}}{}
-\IfFileExists{\AA@bibEndnote}{\setboolean{AA@bibExists}{true}}{}
-\IfFileExists{\AA@bibRIS}{\setboolean{AA@bibExists}{true}}{}
-
 \setlength\AA@x{1in+\hoffset+\oddsidemargin}
 
 \newcommand{\authorcrfont}{\footnotesize}
@@ -148,8 +169,7 @@
 %%%% LNCS
 \ifAA@LNCS%
   \ifAA@orcidicon%
-    \renewcommand{\orcidID}[1]{\href{https://orcid.org/#1}{%
-      \textsuperscript{\,\includegraphics[height=2\fontcharht\font`A]{vector_iD_icon}}}}
+    \renewcommand{\orcidID}[1]{\orcidlink{#1}}
   \else\relax\fi%
 %  
   \ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
@@ -157,23 +177,11 @@
   }{}
   \renewcommand{\authorcrfont}{\scriptsize}
   \@ifclasswith{llncs}{a4paper}{%
-    \ExplSyntaxOn
-    \@ifundefined{pdfmanagement_add:nnn}{%
-      \pdfpagesattr{/CropBox [92 114 523 780]}%
-    }{%
-      \pdfmanagement_add:nnn {Pages}{CropBox}{[92~114~523~780]}
-    }%
-    \ExplSyntaxOff
+    \AA@pdfpagesattribute{CropBox}{[92 114 523 780]}%
     \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},40){#1}}%
   }{%
-    \ExplSyntaxOn
-    \@ifundefined{pdfmanagement_add:nnn}{%
-      \pdfpagesattr{/CropBox [92 65 523 731]}% LNCS page: 152x235 mm
-    }{%
-      \pdfmanagement_add:nnn {Pages}{CropBox}{[92~62~523~731]}
-    }%
-    \ExplSyntaxOff
-    \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},23){#1}}
+    \AA@pdfpagesattribute{CropBox}{[92 65 523 731]}%
+    \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},23){#1}}%
   }
   \setlength{\AA@width}{\textwidth}
   \setcounter{tocdepth}{2}
@@ -186,7 +194,7 @@
   }{}
   \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},35){#1}}
   \renewcommand{\authorcrfont}{\scriptsize}
-  \pdfpagesattr{/CropBox [70 65 526.378 748.15]} % TODO
+  \AA@pdfpagesattribute{CropBox}{[70 65 526.378 748.15]}
   \setlength{\AA@width}{\textwidth}
   \setcounter{tocdepth}{2}
 \fi
@@ -218,8 +226,6 @@
   draft         = false,
   bookmarksopen = true,
   bookmarksnumbered= true,
-  pdfauthor     = {\@author},
-  pdftitle      = {\@title},
 }
 
 \@ifpackageloaded{totpages}{%
@@ -305,26 +311,26 @@
           \hfill
           \begin{itemize*}[label={}, itemjoin={,}]
             \IfFileExists{\AA@bibBibTeX}{%
-              \item \attachandlink{\AA@bibBibTeX}[application/x-bibtex]{BibTeX entry of this paper}{\BibTeX}%
+              \item \expanded{\attachandlink[\AA@key.bib]{\AA@bibBibTeX}[application/x-bibtex]{BibTeX entry of this paper}{\BibTeX}}%
             }{%
               \IfFileExists{\AA@bibBibTeXLong}{%
-                \item \attachandlink[\AA@key.bib]{\AA@bibBibTeXLong}[application/x-bibtex]{BibTeX entry of this paper}{\BibTeX}%
+                \item \expanded{\attachandlink[\AA@key.bib]{\AA@bibBibTeXLong}[application/x-bibtex]{BibTeX entry of this paper}{\BibTeX}}%
               }{%
                 \typeout{No file \AA@bibBibTeX{} (and no \AA@bibBibTeXLong) found. Not embedded reference in BibTeX format.}%
               }%
             }%
             \IfFileExists{\AA@bibWord}{%
-              \item \attachandlink{\AA@bibWord}[application/xml]{XML entry of this paper (e.g., for Word 2007 and later)}{Word}%
+              \item \expanded{\attachandlink[\AA@key.word.xml]{\AA@bibWord}[application/xml]{XML entry of this paper (e.g., for Word 2007 and later)}{Word}}%
             }{%
               \typeout{No file \AA@bibWord{} found. Not embedded reference for Word 2007 and later.}%
             }%
             \IfFileExists{\AA@bibEndnote}{%
-              \item \attachandlink{\AA@bibEndnote}[application/x-endnote-refer]{Endnote entry of this paper}{EndNote}%
+              \item \expanded{\attachandlink[\AA@key.enw]{\AA@bibEndnote}[application/x-endnote-refer]{Endnote entry of this paper}{EndNote}}%
             }{%
               \typeout{No file \AA@bibEndnote{} found. Not embedded reference in Endnote format.}%
             }%
             \IfFileExists{\AA@bibRIS}{%
-              \item \attachandlink{\AA@bibRIS}[application/x-research-info-systems]{RIS entry of this paper}{RIS}%
+              \item \expanded{\attachandlink[\AA@key.ris]{\AA@bibRIS}[application/x-research-info-systems]{RIS entry of this paper}{RIS}}%
             }{%
               \typeout{No file \AA@bibRIS{} found. Not embedded reference in RIS format.}%
             }%

Isabelle_DOF-Example-I/document/lstisadof-manual.sty

@@ -90,9 +90,7 @@
      ,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
+     %,before skip balanced=0.5\baselineskip plus 2pt % works only with Tex Live 2020 and later
      ,enlarge top by=0mm
      ,enhanced
      ,overlay={\node[draw,fill=isar!60!black,xshift=0pt,anchor=north
@@ -136,11 +134,12 @@
 \lstloadlanguages{ML}
 \providecolor{sml}{named}{red}
 \lstdefinestyle{sml}{
-   basicstyle=\ttfamily,%
-   commentstyle=\itshape,%
-   keywordstyle=\bfseries\color{CornflowerBlue},%
-   ndkeywordstyle=\color{green},%
-   language=ML
+   ,escapechar=ë%
+   ,basicstyle=\ttfamily%
+   ,commentstyle=\itshape%
+   ,keywordstyle=\bfseries\color{CornflowerBlue}%
+   ,ndkeywordstyle=\color{green}%
+   ,language=ML
 %  ,literate={%
 %     {<@>}{@}1%
 %    }
@@ -150,7 +149,7 @@
    ,tagstyle=\color{CornflowerBlue}%
    ,markfirstintag=true%
 }%
-\def\inlinesml{\lstinline[style=sml,breaklines=true,mathescape,breakatwhitespace=true]}
+\def\inlinesml{\lstinline[style=sml,breaklines=true,breakatwhitespace=true]}
 \newtcblisting{sml}[1][]{%
       listing only%
      ,boxrule=0pt
@@ -170,7 +169,6 @@
           style=sml
           ,columns=flexible%
           ,basicstyle=\small\ttfamily
-          ,mathescape
           ,#1
       }
   }%
@@ -296,3 +294,34 @@
   }%
 %% </bash>
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%% <config>
+\providecolor{config}{named}{gray}
+\newtcblisting{config}[2][]{%
+      listing only%
+     ,boxrule=0pt
+     ,boxsep=0pt
+     ,colback=white!90!config
+     ,enhanced jigsaw
+     ,borderline west={2pt}{0pt}{config!60!black}
+     ,sharp corners
+     % ,before skip=10pt
+     % ,after skip=10pt
+     ,enlarge top by=0mm
+     ,enhanced
+     ,overlay={\node[draw,fill=config!60!black,xshift=0pt,anchor=north
+       east,font=\bfseries\footnotesize\color{white}]
+                at (frame.north east) {#2};}
+        ,listing options={
+           breakatwhitespace=true
+          ,columns=flexible%
+          ,basicstyle=\small\ttfamily
+          ,mathescape
+          ,#1
+      }
+  }%
+%% </config>
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+

Isabelle_DOF-Example-I/document/preamble.tex

@@ -20,39 +20,9 @@
 \usepackage{xcolor}
 \usepackage{paralist}
 \usepackage{listings}
-\usepackage{lstisadof}
-\usepackage{xspace}
-
-\lstloadlanguages{bash}
-\lstdefinestyle{bash}{language=bash,
-  ,basicstyle=\ttfamily%
-  ,showspaces=false%
-  ,showlines=false%
-  ,columns=flexible%
- %  ,keywordstyle=\bfseries%
-   % Defining 2-keywords
-   ,keywordstyle=[1]{\color{BrickRed!60}\bfseries}%
-   % Defining 3-keywords
-   ,keywordstyle=[2]{\color{OliveGreen!60}\bfseries}%
-   % Defining 4-keywords
-   ,keywordstyle=[3]{\color{black!60}\bfseries}%
-   % Defining 5-keywords
-   ,keywordstyle=[4]{\color{Blue!70}\bfseries}%
-   % Defining 6-keywords
-   ,keywordstyle=[5]{\itshape}%
-  % 
-}
-\lstdefinestyle{displaybash}{style=bash,
-                basicstyle=\ttfamily\footnotesize,
-                backgroundcolor=\color{black!2}, frame=lines}%
-
-\lstnewenvironment{bash}[1][]{\lstset{style=displaybash, #1}}{}
-\def\inlinebash{\lstinline[style=bash, breaklines=true,columns=fullflexible]}
-
-\usepackage[caption]{subfig}
-\usepackage[size=footnotesize]{caption}
-
+\usepackage{lstisadof-manual}
 
+\providecommand{\isactrlemph}[1]{\emph{#1}}
 \usepackage[LNCS,
    orcidicon,
    key=brucker.ea-isabelle-ontologies-2018,

Isabelle_DOF-Example-II/ROOT

@@ -1,5 +1,7 @@
-session "2020-iFM-csp" = "Isabelle_DOF" +
-  options [document = pdf, document_output = "output", document_build = dof]
+chapter AFP 
+
+session "Isabelle_DOF-Example-II" (AFP) = "Isabelle_DOF" +
+  options [document = pdf, document_output = "output", document_build = dof, timeout = 300]
   theories
     "paper"
   document_files

Isabelle_DOF-Example-II/document/preamble.tex

@@ -1,6 +1,8 @@
 %% This is a placeholder for user-specific configuration and packages.
 
 \usepackage{stmaryrd}
+\usepackage{pifont}% http://ctan.org/pkg/pifont
+
 
 \title{<TITLE>}
 \author{<AUTHOR>}

Isabelle_DOF-Example-II/paper.thy

@@ -12,10 +12,13 @@ declare[[ strict_monitor_checking  = false]]
 declare[[ Definition_default_class = "definition"]]
 declare[[ Lemma_default_class      = "lemma"]]
 declare[[ Theorem_default_class    = "theorem"]]
+declare[[ Corollary_default_class  = "corollary"]]
 
 define_shortcut* csp      \<rightleftharpoons> \<open>CSP\<close>
                  holcsp   \<rightleftharpoons> \<open>HOL-CSP\<close>
                  isabelle \<rightleftharpoons> \<open>Isabelle/HOL\<close>
+                 hfill    \<rightleftharpoons> \<open>\hfill\<close>
+                 br    \<rightleftharpoons> \<open>\break\<close>
 
 (*>*)
 
@@ -27,7 +30,7 @@ author*[lina,email="\<open>lina.ye@lri.fr\<close>",affiliation="\<open>LRI, Inri
                
 abstract*[abs, keywordlist="[\<open>Shallow Embedding\<close>,\<open>Process-Algebra\<close>,
                              \<open>Concurrency\<close>,\<open>Computational Models\<close>]"]
-\<open>  The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today 
+\<open>  The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today  
    one of the reference theories for concurrent specification and computing. In 1997, a first 
    formalization in \<^isabelle> of the denotational semantics of the  Failure/Divergence Model of
    \<^csp> was undertaken; in particular, this model can cope with infinite alphabets, in contrast 
@@ -51,33 +54,32 @@ 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(@{author ''bu''}::author)"]\<open> Introduction \<close> 
 text*[introtext::introduction, level="Some 1"]\<open>
-Communicating Sequential Processes (\<^csp>) is a language 
-to specify and verify patterns of interaction of concurrent systems.
-Together with CCS and LOTOS, it belongs to the family of \<^emph>\<open>process algebras\<close>. 
-\<^csp>'s rich theory comprises denotational, operational and algebraic semantic facets 
-and has influenced programming languages such as Limbo, Crystal, Clojure and
-most notably Golang @{cite "donovan2015go"}. \<^csp> has been applied in 
-industry as a tool for specifying and verifying the concurrent aspects of hardware 
-systems, such as the T9000 transansputer @{cite "Barret95"}. 
+Communicating Sequential Processes (\<^csp>) is a language to specify and verify patterns of 
+interaction of concurrent systems. Together with CCS and LOTOS, it belongs to the family of 
+\<^emph>\<open>process algebras\<close>. \<^csp>'s rich theory comprises denotational, operational and algebraic semantic 
+facets and has influenced programming languages such as Limbo, Crystal, Clojure and most notably 
+Golang @{cite "donovan2015go"}. \<^csp> has been applied in industry as a tool for specifying and 
+verifying the concurrent aspects of hardware systems, such as the T9000 transansputer 
+@{cite "Barret95"}. 
 
 The theory of \<^csp> was first described in 1978 in a book by Tony Hoare @{cite "Hoare:1985:CSP:3921"}, 
 but has since evolved substantially @{cite "BrookesHR84" and "brookes-roscoe85" and "roscoe:csp:1998"}.
-\<^csp> describes the most common communication and synchronization mechanisms
-with one single language primitive: synchronous communication written \<open>_\<lbrakk>_\<rbrakk>_\<close>. \<^csp> semantics is 
-described by a fully abstract model of behaviour designed to be \<^emph>\<open>compositional\<close>: the denotational
-semantics of a process \<open>P\<close> encompasses all possible behaviours of this process in the context of all 
-possible environments \<open>P \<lbrakk>S\<rbrakk> Env\<close> (where \<open>S\<close> is the set of \<open>atomic events\<close> both \<open>P\<close> and \<open>Env\<close> must
-synchronize). This design objective has the consequence that two kinds of choice have to 
-be distinguished: 
-  \<^enum> the \<^emph>\<open>external choice\<close>, written \<open>_\<box>_\<close>, which forces a process "to follow" whatever
-    the environment offers, and
-  \<^enum> the \<^emph>\<open>internal choice\<close>, written \<open>_\<sqinter>_\<close>, which imposes on the environment of a process 
-    "to follow" the non-deterministic choices made.
+\<^csp> describes the most common communication and synchronization mechanisms with one single language 
+primitive: synchronous communication written \<open>_\<lbrakk>_\<rbrakk>_\<close>. \<^csp> semantics is described by a fully abstract 
+model of behaviour designed to be \<^emph>\<open>compositional\<close>: the denotational semantics of a process \<open>P\<close> 
+encompasses all possible behaviours of this process in the context of all possible environments 
+\<open>P \<lbrakk>S\<rbrakk> Env\<close> (where \<open>S\<close> is the set of \<open>atomic events\<close> both \<open>P\<close> and \<open>Env\<close> must synchronize). This 
+design objective has the consequence that two kinds of choice have to be distinguished: \<^vs>\<open>0.1cm\<close>
 
+  \<^enum> the \<^emph>\<open>external choice\<close>, written \<open>_\<box>_\<close>, which forces a process "to follow" whatever
+    the environment offers, and \<^vs>\<open>-0.4cm\<close>
+  \<^enum> the \<^emph>\<open>internal choice\<close>, written \<open>_\<sqinter>_\<close>, which imposes on the environment of a process 
+    "to follow" the non-deterministic choices made.\<^vs>\<open>0.3cm\<close>
 \<close>
-text\<open>
+
+text\<open> \<^vs>\<open>-0.6cm\<close>
 Generalizations of these two operators \<open>\<box>x\<in>A. P(x)\<close> and \<open>\<Sqinter>x\<in>A. P(x)\<close> allow for modeling the concepts 
 of \<^emph>\<open>input\<close> and \<^emph>\<open>output\<close>: Based on the prefix operator \<open>a\<rightarrow>P\<close> (event \<open>a\<close> happens, then the process 
 proceeds with \<open>P\<close>), receiving input is modeled by \<open>\<box>x\<in>A. x\<rightarrow>P(x)\<close> while sending output is represented 
@@ -123,25 +125,11 @@ attempt to formalize denotational \<^csp> semantics covering a part of Bill Rosc
     \<^url>\<open>https://gitlri.lri.fr/burkhart.wolff/hol-csp2.0\<close>. In this paper, all Isabelle proofs are 
     omitted.\<close>}. 
 \<close>
-(*
-% Moreover, decomposition rules of the form:
-% \begin{center}
-% \begin{minipage}[c]{10cm}
-%    @{cartouche [display] \<open>C \<Longrightarrow> A \<sqsubseteq>\<^sub>F\<^sub>D A' \<Longrightarrow> B \<sqsubseteq>\<^sub>F\<^sub>D B' \<Longrightarrow> A \<lbrakk>S\<rbrakk> B \<sqsubseteq>\<^sub>F\<^sub>D A' \<lbrakk>S\<rbrakk> B'\<close>}
-% \end{minipage}
-% \end{center} 
-% are of particular interest since they allow to avoid the costly automata-product construction 
-% of model-checkers and to separate infinite sub-systems from finite (model-checkable) ones; however,
-% their side-conditions \<open>C\<close> are particularly tricky to work out. Decomposition rules  may pave the 
-% way for future tool combinations for model-checkers such as FDR4~@{cite "fdr4"} or 
-% PAT~@{cite "SunLDP09"} based on proof certifications.*)
 
-section*["pre"::tc,main_author="Some(@{docitem \<open>bu\<close>}::author)"]
+section*["pre"::technical,main_author="Some(@{author \<open>bu\<close>}::author)"]
 \<open>Preliminaries\<close>
 
-text\<open>\<close>
-
-subsection*[cspsemantics::tc, main_author="Some(@{docitem ''bu''})"]\<open>Denotational \<^csp> Semantics\<close>
+subsection*[cspsemantics::technical, main_author="Some(@{author ''bu''})"]\<open>Denotational \<^csp> Semantics\<close>
 
 text\<open> The denotational semantics (following @{cite "roscoe:csp:1998"}) comes in three layers: 
 the \<^emph>\<open>trace model\<close>, the \<^emph>\<open>(stable) failures model\<close> and the \<^emph>\<open>failure/divergence model\<close>.
@@ -155,9 +143,9 @@ processes \<open>Skip\<close> (successful termination) and \<open>Stop\<close> (
 Note that the trace sets, representing all \<^emph>\<open>partial\<close> history, is in general prefix closed.\<close>
 
 text*[ex1::math_example, status=semiformal, level="Some 1"] \<open>
-Let two processes be defined as follows:
+Let two processes be defined as follows:\<^vs>\<open>0.2cm\<close>
 
-  \<^enum>  \<open>P\<^sub>d\<^sub>e\<^sub>t = (a \<rightarrow> Stop) \<box> (b \<rightarrow> Stop)\<close>
+  \<^enum> \<open>P\<^sub>d\<^sub>e\<^sub>t = (a \<rightarrow> Stop) \<box> (b \<rightarrow> Stop)\<close>
   \<^enum> \<open>P\<^sub>n\<^sub>d\<^sub>e\<^sub>t = (a \<rightarrow> Stop) \<sqinter> (b \<rightarrow> Stop)\<close> 
 \<close> 
 
@@ -183,7 +171,6 @@ The following process \<open>P\<^sub>i\<^sub>n\<^sub>f\<close> is an infinite pr
 many times. However, using the \<^csp> hiding operator \<open>_\_\<close>, this activity is concealed: 
 
   \<^enum>  \<open>P\<^sub>i\<^sub>n\<^sub>f = (\<mu> X. a \<rightarrow> X) \ {a}\<close>
-
 \<close>
 
 text\<open>where \<open>P\<^sub>i\<^sub>n\<^sub>f\<close> will be equivalent to \<open>\<bottom>\<close> in the process cpo ordering. 
@@ -202,7 +189,7 @@ of @{cite "IsobeRoggenbach2010"} is restricted to a variant of the failures mode
  
 \<close>
 
-subsection*["isabelleHol"::tc, main_author="Some(@{docitem ''bu''})"]\<open>Isabelle/HOL\<close>
+subsection*["isabelleHol"::technical, main_author="Some(@{author ''bu''})"]\<open>Isabelle/HOL\<close>
 text\<open> Nowadays, Isabelle/HOL is one of the major interactive theory development environments
 @{cite "nipkow.ea:isabelle:2002"}. HOL stands for Higher-Order Logic, a logic based on simply-typed
 \<open>\<lambda>\<close>-calculus extended by parametric polymorphism and Haskell-like type-classes.
@@ -214,7 +201,6 @@ in the plethora of work done and has been a key factor for the success of the Ar
 For the work presented here, one relevant construction is :
 
    \<^item> \<^theory_text>\<open>typedef  (\<alpha>\<^sub>1,...,\<alpha>\<^sub>n)t = E\<close>
-
  
 It creates a fresh type that is isomorphic to a set \<open>E\<close> involving \<open>\<alpha>\<^sub>1,...,\<alpha>\<^sub>n\<close> types.
 Isabelle/HOL performs a number of syntactic checks for these constructions that guarantee the logical
@@ -225,25 +211,23 @@ distribution comes with rich libraries comprising Sets, Numbers, Lists, etc. whi
 For this work, a particular library called \<^theory_text>\<open>HOLCF\<close> is intensively used. It provides classical 
 domain theory for a particular type-class \<open>\<alpha>::pcpo\<close>, \<^ie> the class of types  \<open>\<alpha>\<close> for which 
 
-   \<^enum>  a least element \<open>\<bottom>\<close> is defined, and
+   \<^enum> a least element \<open>\<bottom>\<close> is defined, and
    \<^enum> a complete partial order \<open>_\<sqsubseteq>_\<close> is defined.
 
  For these types, \<^theory_text>\<open>HOLCF\<close> provides a fixed-point operator \<open>\<mu>X. f X\<close> as well as the 
 fixed-point induction and other (automated) proof infrastructure. Isabelle's type-inference can 
 automatically infer, for example, that if \<open>\<alpha>::pcpo\<close>, then \<open>(\<beta> \<Rightarrow> \<alpha>)::pcpo\<close>. \<close>
   
-section*["csphol"::tc,main_author="Some(@{docitem ''bu''}::author)", level="Some 2"]
+section*["csphol"::technical,main_author="Some(@{author ''bu''}::author)", level="Some 2"]
 \<open>Formalising Denotational \<^csp> Semantics in HOL \<close>
 
-text\<open>\<close>
-
-subsection*["processinv"::tc, main_author="Some(@{docitem ''bu''})"]
+subsection*["processinv"::technical, main_author="Some(@{author ''bu''})"]
 \<open>Process Invariant and Process Type\<close>
 text\<open> First, we need a slight revision of the concept
 of \<^emph>\<open>trace\<close>: if \<open>\<Sigma>\<close> is the type of the atomic events (represented by a type variable), then
-we need to extend this type by a special event \<open>\<surd>\<close> (called "tick") signaling termination.
-Thus, traces have the type \<open>(\<Sigma>+\<surd>)\<^sup>*\<close>, written \<open>\<Sigma>\<^sup>\<surd>\<^sup>*\<close>; since \<open>\<surd>\<close> may only occur at the end of a trace, 
-we need to define a predicate \<open>front\<^sub>-tickFree t\<close> that requires from traces that \<open>\<surd>\<close> can only occur 
+we need to extend this type by a special event \<open>\<checkmark>\<close> (called "tick") signaling termination.
+Thus, traces have the type \<open>(\<Sigma>\<uplus>\<checkmark>)\<^sup>*\<close>, written \<open>\<Sigma>\<^sup>\<checkmark>\<^sup>*\<close>; since \<open>\<checkmark>\<close> may only occur at the end of a trace, 
+we need to define a predicate \<open>front\<^sub>-tickFree t\<close> that requires from traces that \<open>\<checkmark>\<close> can only occur 
 at the end.
 
 Second, in the traditional literature, the semantic domain is implicitly described by 9 "axioms" 
@@ -258,38 +242,37 @@ Informally, these are:
    \<^item> the tick accepted after a trace \<open>s\<close> implies that all other events are refused; 
    \<^item> a divergence trace with any suffix is itself a divergence one
    \<^item> once a process has diverged, it can engage in or refuse any sequence of events.
-   \<^item> a trace ending with \<open>\<surd>\<close> belonging to divergence set implies that its 
-     maximum prefix without \<open>\<surd>\<close> is also a divergent trace.
+   \<^item> a trace ending with \<open>\<checkmark>\<close> belonging to divergence set implies that its 
+     maximum prefix without \<open>\<checkmark>\<close> is also a divergent trace.
 
 More formally, a process \<open>P\<close> of the type \<open>\<Sigma> process\<close> should have the following properties:
 
-
-@{cartouche [display] \<open>([],{}) \<in> \<F> P \<and>
+@{cartouche [display, indent=10] \<open>([],{}) \<in> \<F> P \<and>
 (\<forall> s X.  (s,X) \<in> \<F> P \<longrightarrow> front_tickFree s) \<and>
 (\<forall> s t . (s@t,{}) \<in> \<F> P \<longrightarrow> (s,{}) \<in> \<F> P) \<and>
 (\<forall> s X Y. (s,Y) \<in> \<F> P \<and> X\<subseteq>Y \<longrightarrow> (s,X) \<in> \<F> P) \<and> 
 (\<forall> s X Y. (s,X) \<in> \<F> P \<and> (\<forall>c \<in> Y. ((s@[c],{}) \<notin> \<F> P)) \<longrightarrow> (s,X \<union> Y) \<in> \<F> P) \<and>
-(\<forall> s X.  (s@[\<surd>],{}) \<in> \<F> P \<longrightarrow> (s,X-{\<surd>}) \<in> \<F> P) \<and>
+(\<forall> s X.  (s@[\<checkmark>],{}) \<in> \<F> P \<longrightarrow> (s,X-{\<checkmark>}) \<in> \<F> P) \<and>
 (\<forall> s t. s \<in> \<D> P \<and> tickFree s \<and> front_tickFree t \<longrightarrow> s@t \<in> \<D> P)  \<and>
 (\<forall> s X. s \<in> \<D> P \<longrightarrow> (s,X) \<in> \<F> P) \<and>
-(\<forall> s. s@[\<surd>] \<in> \<D> P \<longrightarrow> s \<in> \<D> P)\<close>}
+(\<forall> s. s@[\<checkmark>] \<in> \<D> P \<longrightarrow> s \<in> \<D> P)\<close>}
 
 Our objective is to encapsulate this wishlist into a type constructed as a conservative
 theory extension in our theory \<^holcsp>.
-Therefore third, we define a pre-type for processes \<open>\<Sigma> process\<^sub>0\<close> by \<open> \<P>(\<Sigma>\<^sup>\<surd>\<^sup>* \<times> \<P>(\<Sigma>\<^sup>\<surd>)) \<times> \<P>(\<Sigma>\<^sup>\<surd>)\<close>.
+Therefore third, we define a pre-type for processes \<open>\<Sigma> process\<^sub>0\<close> by \<open> \<P>(\<Sigma>\<^sup>\<checkmark>\<^sup>* \<times> \<P>(\<Sigma>\<^sup>\<checkmark>)) \<times> \<P>(\<Sigma>\<^sup>\<checkmark>)\<close>.
 Forth, we turn our wishlist of "axioms" above into the definition of a predicate \<open>is_process P\<close> 
 of type \<open>\<Sigma> process\<^sub>0 \<Rightarrow> bool\<close> deciding if its conditions are fulfilled. Since \<open>P\<close> is a pre-process,
 we replace \<open>\<F>\<close> by \<open>fst\<close> and  \<open>\<D>\<close> by \<open>snd\<close> (the HOL projections into a pair).
 And last not least fifth, we use the following type definition:
-  \<^item> \<^theory_text>\<open>typedef '\<alpha> process = "{P :: '\<alpha> process\<^sub>0 . is_process P}"\<close>
 
+  \<^item> \<^theory_text>\<open>typedef '\<alpha> process = "{P :: '\<alpha> process\<^sub>0 . is_process P}"\<close>
 
 Isabelle requires a proof for the existence of a witness for this set,
 but this can be constructed in a straight-forward manner. Suitable definitions for 
 \<open>\<T>\<close>, \<open>\<F>\<close> and \<open>\<D>\<close> lifting \<open>fst\<close> and \<open>snd\<close> on the new \<open>'\<alpha> process\<close>-type allows to derive
 the above properties for any \<open>P::'\<alpha> process\<close>. \<close>
 
-subsection*["operator"::tc, main_author="Some(@{docitem ''lina''})"]
+subsection*["operator"::technical, main_author="Some(@{author ''lina''})"]
 \<open>\<^csp> Operators over the Process Type\<close>
 text\<open> Now, the operators of \<^csp> \<open>Skip\<close>, \<open>Stop\<close>, \<open>_\<sqinter>_\<close>,  \<open>_\<box>_\<close>, \<open>_\<rightarrow>_\<close>,\<open>_\<lbrakk>_\<rbrakk>_\<close> etc. 
 for internal choice, external choice, prefix and parallel composition, can 
@@ -303,17 +286,18 @@ For example, we define \<open>_\<sqinter>_\<close> on the pre-process type as fo
 
   \<^item> \<^theory_text>\<open>definition "P \<sqinter> Q \<equiv> Abs_process(\<F> P \<union> \<F> Q , \<D> P \<union> \<D> Q)"\<close>
 
-where \<open>\<F> = fst \<circ> Rep_process\<close> and \<open>\<D> = snd \<circ> Rep_process\<close> and where \<open>Rep_process\<close> and
-\<open>Abs_process\<close> are the representation and abstraction morphisms resulting from the
-type definition linking \<open>'\<alpha> process\<close> isomorphically to \<open>'\<alpha> process\<^sub>0\<close>. Proving the above properties
-for  \<open>\<F> (P \<sqinter> Q)\<close> and \<open>\<D> (P \<sqinter> Q)\<close> requires a proof that \<open>(\<F> P \<union> \<F> Q , \<D> P \<union> \<D> Q)\<close>
-satisfies the 9 "axioms", which is fairly simple in this case.
+where \<open>Rep_process\<close> and \<open>Abs_process\<close> are the representation and abstraction morphisms resulting 
+from the type definition linking the type \<open>'\<alpha> process\<close> isomorphically to the set \<open>'\<alpha> process\<^sub>0\<close>. 
+The projection into \<^emph>\<open>failures\<close> is defined by \<open>\<F> = fst \<circ> Rep_process\<close>, whereas the 
+\<^emph>\<open>divergences\<close> are defined bz \<open>\<D> = snd \<circ> Rep_process\<close>. Proving the above properties for  
+\<open>\<F> (P \<sqinter> Q)\<close> and \<open>\<D> (P \<sqinter> Q)\<close> requires a proof that \<open>(\<F> P \<union> \<F> Q , \<D> P \<union> \<D> Q)\<close>
+satisfies the well-formedness conditions of \<open>is_process\<close>, which is fairly simple in this case.
 
 The definitional presentation of the \<^csp> process operators according to @{cite "roscoe:csp:1998"} 
 follows always this scheme. This part of the theory comprises around 2000 loc. 
 \<close>
 
-subsection*["orderings"::tc, main_author="Some(@{docitem ''bu''})"]
+subsection*["orderings"::technical, main_author="Some(@{author ''bu''})"]
 \<open>Refinement Orderings\<close>
 
 text\<open> \<^csp> is centered around the idea of process refinement; many critical properties, 
@@ -322,15 +306,16 @@ a conversion of processes in terms of (finite) labelled transition systems leads
 model-checking techniques based on graph-exploration. Essentially,  a process \<open>P\<close> \<^emph>\<open>refines\<close> 
 another process \<open>Q\<close> if and only if it is more deterministic and more defined (has less divergences).
 Consequently, each of the three semantics models (trace, failure and failure/divergence) 
-has its corresponding refinement orderings. 
+has its corresponding refinement orderings.\<close>
+Theorem*[th1::"theorem", short_name="\<open>Refinement properties\<close>"]\<open>
 What we are interested in this paper is the following refinement orderings for the 
 failure/divergence model.
 
    \<^enum> \<open>P \<sqsubseteq>\<^sub>\<F>\<^sub>\<D> Q \<equiv> \<F> P \<supseteq> \<F> Q \<and> \<D> P \<supseteq> \<D> Q\<close> 
    \<^enum> \<open>P \<sqsubseteq>\<^sub>\<T>\<^sub>\<D> Q \<equiv> \<T> P \<supseteq> \<T> Q \<and> \<D> P \<supseteq> \<D> Q\<close>
-   \<^enum> \<open>P \<sqsubseteq>\<^sub>\<FF> Q \<equiv>  \<FF> P \<supseteq> \<FF> Q, \<FF>\<in>{\<T>,\<F>,\<D>}\<close> 
+   \<^enum> \<open>P \<sqsubseteq>\<^sub>\<FF> Q \<equiv>  \<FF> P \<supseteq> \<FF> Q, \<FF>\<in>{\<T>,\<F>,\<D>}\<close>  \<close>
 
- Notice that in the \<^csp> literature, only \<open>\<sqsubseteq>\<^sub>\<F>\<^sub>\<D>\<close> is well studied for failure/divergence model. 
+text\<open> Notice that in the \<^csp> literature, only \<open>\<sqsubseteq>\<^sub>\<F>\<^sub>\<D>\<close> is well studied for failure/divergence model. 
 Our formal analysis of different granularities on the refinement orderings   
 allows deeper understanding of the same semantics model. For example, \<open>\<sqsubseteq>\<^sub>\<T>\<^sub>\<D>\<close> turns
 out to have in some cases better monotonicity properties and therefore allow for stronger proof
@@ -342,7 +327,7 @@ states, from which no internal progress is possible.
 \<close>
 
 
-subsection*["fixpoint"::tc, main_author="Some(@{docitem ''lina''})"]
+subsection*["fixpoint"::technical, main_author="Some(@{author ''lina''})"]
 \<open>Process Ordering and HOLCF\<close>
 text\<open> For any denotational semantics, the fixed point theory giving semantics to systems
 of recursive equations is considered as keystone. Its prerequisite is a complete partial ordering
@@ -356,15 +341,14 @@ is based on the concept \<^emph>\<open>refusals after\<close> a trace \<open>s\<
 
 Definition*[process_ordering, level= "Some 2", short_name="''process ordering''"]\<open>
 We define \<open>P \<sqsubseteq> Q \<equiv> \<psi>\<^sub>\<D> \<and> \<psi>\<^sub>\<R> \<and> \<psi>\<^sub>\<M> \<close>,  where 
-\<^enum>  \<open>\<psi>\<^sub>\<D> = \<D> P \<supseteq> \<D> Q \<close>
+\<^enum> \<open>\<psi>\<^sub>\<D> = \<D> P \<supseteq> \<D> Q \<close>
 \<^enum> \<open>\<psi>\<^sub>\<R> = s \<notin> \<D> P \<Rightarrow> \<R> P s = \<R> Q s\<close>  
-\<^enum> \<open>\<psi>\<^sub>\<M> = Mins(\<D> P) \<subseteq> \<T> Q \<close> 
-\<close>
+\<^enum> \<open>\<psi>\<^sub>\<M> = Mins(\<D> P) \<subseteq> \<T> Q \<close> \<close>
 
 text\<open>The third condition \<open>\<psi>\<^sub>\<M>\<close> implies that the set of minimal divergent traces 
 (ones with no proper prefix that is also a divergence) in  \<open>P\<close>,  denoted by \<open>Mins(\<D> P)\<close>, 
 should be a subset of the trace set of \<open>Q\<close>. 
-%One may note that each element in \<open>Mins(\<D> P)\<close> do actually not contain the \<open>\<surd>\<close>, 
+%One may note that each element in \<open>Mins(\<D> P)\<close> do actually not contain the \<open>\<checkmark>\<close>, 
 %which can be deduced from the process invariants described 
 %in the precedent @{technical "processinv"}. This can be explained by the fact that we are not 
 %really concerned with what a process does after it terminates. 
@@ -395,44 +379,45 @@ For most \<^csp> operators \<open>\<otimes>\<close> we derived rules of the form
 
 These rules allow to automatically infer for any process term if it is continuous or not.  
 The port of HOL-CSP 2 on HOLCF implied that the derivation of the entire continuity rules 
-had to be completely re-done (3000 loc).
-
- 
-HOL-CSP provides an important proof principle, the fixed-point induction:
+had to be completely re-done (3000 loc).\<close>
 
+Theorem*[th2,short_name="\<open>Fixpoint Induction\<close>"]
+\<open>HOL-CSP provides an important proof principle, the fixed-point induction:
 @{cartouche [display, indent=5] \<open>cont f \<Longrightarrow> adm P \<Longrightarrow> P \<bottom> \<Longrightarrow> (\<And>X. P X \<Longrightarrow> P(f X)) \<Longrightarrow> P(\<mu>X. f X)\<close>}
+\<close>
 
-Fixed-point induction requires a small side-calculus for establishing the admissibility
+text\<open>Fixed-point induction of @{theorem th2} requires a small side-calculus for establishing the admissibility
 of a predicate; basically, predicates are admissible if they are valid for any least upper bound 
 of a chain \<open>x\<^sub>1 \<sqsubseteq> x\<^sub>2 \<sqsubseteq> x\<^sub>3 ... \<close> provided that \<open>\<forall>i. P(x\<^sub>i)\<close>. It turns out that \<open>_\<sqsubseteq>_\<close> and \<open>_\<sqsubseteq>\<^sub>F\<^sub>D_\<close> as
 well as all other refinement orderings that we introduce in this paper are  admissible.
-Fixed-point inductions are the main proof weapon in verifications, 
-together with monotonicities and the \<^csp> laws. Denotational arguments can be hidden as they are not 
-needed in practical verifications. \<close>
+Fixed-point inductions are the main proof weapon in verifications, together with monotonicities 
+and the \<^csp> laws. Denotational arguments can be hidden as they are not needed in practical 
+verifications. \<close>
 
-subsection*["law"::tc, main_author="Some(@{docitem ''lina''})"]
+subsection*["law"::technical, main_author="Some(@{author ''lina''})"]
 \<open>\<^csp> Rules: Improved Proofs and New Results\<close>
 
 
-text\<open> The \<^csp> operators enjoy a number of algebraic properties: commutativity, 
+text\<open>The \<^csp> operators enjoy a number of algebraic properties: commutativity, 
 associativities, and idempotence in some cases. Moreover, there is a rich body of distribution
 laws between these operators. Our new version HOL-CSP 2 not only shortens and restructures the 
-proofs of @{cite "tej.ea:corrected:1997"}; the code reduces  
-to 8000 loc from 25000 loc. Some illustrative examples of new established rules are:
+proofs of @{cite "tej.ea:corrected:1997"}; the code reduces to 8000 loc from 25000 loc. \<close>
 
+Theorem*[th3, short_name="\<open>Examples of Derived Rules.\<close>"]\<open> 
   \<^item> \<open>\<box>x\<in>A\<union>B\<rightarrow>P(x) = (\<box>x\<in>A\<rightarrow>P x) \<box> (\<box>x\<in>B\<rightarrow>P x)\<close>
   \<^item> \<open>A\<union>B\<subseteq>C \<Longrightarrow> (\<box>x\<in>A\<rightarrow>P x \<lbrakk>C\<rbrakk> \<box>x\<in>B\<rightarrow>Q x) = \<box>x\<in>A\<inter>B\<rightarrow>(P x \<lbrakk>C\<rbrakk> Q x)\<close>
   \<^item> @{cartouche [display]\<open>A\<subseteq>C \<Longrightarrow> B\<inter>C={} \<Longrightarrow> 
                (\<box>x\<in>A\<rightarrow>P x \<lbrakk>C\<rbrakk> \<box>x\<in>B\<rightarrow>Q x) = \<box>x\<in>B\<rightarrow>(\<box>x\<in>A\<rightarrow>P x \<lbrakk>C\<rbrakk> Q x)\<close>}
-  \<^item> \<open>finite A \<Longrightarrow> A\<inter>C = {} \<Longrightarrow> ((P \<lbrakk>C\<rbrakk> Q) \ A) = ((P \ A) \<lbrakk>C\<rbrakk> (Q \ A)) ...\<close>
+  \<^item> \<open>finite A \<Longrightarrow> A\<inter>C = {} \<Longrightarrow> ((P \<lbrakk>C\<rbrakk> Q) \ A) = ((P \ A) \<lbrakk>C\<rbrakk> (Q \ A)) ...\<close>\<close>
 
- The continuity proof of the hiding operator is notorious. The proof is known
-to involve the classical König's lemma stating that every infinite tree with finite branching 
-has an infinite path. We adapt this lemma to our context as follows:
 
- @{cartouche [display, indent=5] 
+text\<open>The continuity proof of the hiding operator is notorious. The proof is known to involve the 
+classical König's lemma stating that every infinite tree with finite branching has an infinite path. 
+We adapt this lemma to our context as follows:
+
+@{cartouche [display, indent=5] 
  \<open>infinite tr \<Longrightarrow> \<forall>i. finite{t. \<exists>t'\<in>tr. t = take i t'} 
-             \<Longrightarrow> \<exists> f. strict_mono f \<and> range f \<subseteq> {t. \<exists>t'\<in>tr. t \<le> t'}\<close>}
+              \<Longrightarrow> \<exists> f. strict_mono f \<and> range f \<subseteq> {t. \<exists>t'\<in>tr. t \<le> t'}\<close>}
 
 in order to come up with the continuity rule: \<open>finite S \<Longrightarrow> cont P \<Longrightarrow> cont(\<lambda>X. P X \ S)\<close>.
 The original proof had been drastically shortened by a factor 10 and important immediate steps
@@ -451,12 +436,12 @@ cases to be considered as well as their complexity makes pen and paper proofs
 practically infeasible.
 \<close>
 
-section*["newResults"::tc,main_author="Some(@{docitem ''safouan''}::author)",
-                                 main_author="Some(@{docitem ''lina''}::author)", level= "Some 3"]
+section*["newResults"::technical,main_author="Some(@{author ''safouan''}::author)",
+                                 main_author="Some(@{author ''lina''}::author)", level= "Some 3"]
 \<open>Theoretical Results on Refinement\<close>
 text\<open>\<close>
-subsection*["adm"::tc,main_author="Some(@{docitem ''safouan''}::author)", 
-                                  main_author="Some(@{docitem ''lina''}::author)"]
+subsection*["adm"::technical,main_author="Some(@{author ''safouan''}::author)", 
+                                  main_author="Some(@{author ''lina''}::author)"]
 \<open>Decomposition Rules\<close>
 text\<open>
 In our framework, we implemented the pcpo process refinement together with the five refinement 
@@ -476,47 +461,23 @@ under all refinement orderings, while others are not.
 \<^item> Sequence operator is not monotonic under \<open>\<sqsubseteq>\<^sub>\<F>\<close>, \<open>\<sqsubseteq>\<^sub>\<D>\<close> or \<open>\<sqsubseteq>\<^sub>\<T>\<close>:
   @{cartouche [display,indent=5] 
     \<open>P \<sqsubseteq>\<^sub>\<FF> P'\<Longrightarrow> Q \<sqsubseteq>\<^sub>\<FF> Q' \<Longrightarrow> (P ; Q) \<sqsubseteq>\<^sub>\<FF> (P' ; Q') where \<FF>\<in>{\<T>\<D>,\<F>\<D>}\<close>}
-%All refinements are right-side monotonic but \<open>\<sqsubseteq>\<^sub>\<F>\<close>, \<open>\<sqsubseteq>\<^sub>\<D>\<close> and \<open>\<sqsubseteq>\<^sub>\<T>\<close> are not left-side monotonic,
-%which can be explained by 
-%the interdependence relationship of failure and divergence projections for the first component. 
-%We thus proved:
+
+All refinements are right-side monotonic but \<open>\<sqsubseteq>\<^sub>\<F>\<close>, \<open>\<sqsubseteq>\<^sub>\<D>\<close> and \<open>\<sqsubseteq>\<^sub>\<T>\<close> are not left-side monotonic,
+which can be explained by the interdependence relationship of failure and divergence projections 
+for the first component. We thus proved:
 \<^item> Hiding operator is not monotonic under \<open>\<sqsubseteq>\<^sub>\<D>\<close>:
   @{cartouche [display,indent=5] \<open>P \<sqsubseteq>\<^sub>\<FF> Q \<Longrightarrow> P \ A  \<sqsubseteq>\<^sub>\<FF> Q \ A where \<FF>\<in>{\<T>,\<F>,\<T>\<D>,\<F>\<D>}\<close>}
-%Intuitively, for the divergence refinement of the hiding operator, there may be
-%some trace \<open>s\<in>\<T> Q\<close> and \<open>s\<notin>\<T> P\<close> such that it becomes divergent in \<open>Q \ A\<close>  but 
-%not in \<open>P \ A\<close>.
-%when the condition in the corresponding projection laws is satisfied, which makes it is not monotonic.
+Intuitively, for the divergence refinement of the hiding operator, there may be
+some trace \<open>s\<in>\<T> Q\<close> and \<open>s\<notin>\<T> P\<close> such that it becomes divergent in \<open>Q \ A\<close>  but 
+not in \<open>P \ A\<close>. 
 \<^item> Parallel composition is not monotonic under \<open>\<sqsubseteq>\<^sub>\<F>\<close>, \<open>\<sqsubseteq>\<^sub>\<D>\<close> or \<open>\<sqsubseteq>\<^sub>\<T>\<close>:
   @{cartouche [display,indent=5] \<open>P \<sqsubseteq>\<^sub>\<FF> P' \<Longrightarrow> Q \<sqsubseteq>\<^sub>\<FF> Q' \<Longrightarrow> (P \<lbrakk>A\<rbrakk> Q) \<sqsubseteq>\<^sub>\<FF> (P' \<lbrakk>A\<rbrakk> Q') where \<FF>\<in>{\<T>\<D>,\<F>\<D>}\<close>}
-%The failure and divergence projections of this operator are also interdependent, similar to the 
-%sequence operator. 
-%Hence, this operator is not monotonic with \<open>\<sqsubseteq>\<^sub>\<F>\<close>, \<open>\<sqsubseteq>\<^sub>\<D>\<close> and \<open>\<sqsubseteq>\<^sub>\<T>\<close>, but monotonic when their 
-%combinations are considered. 
+The failure and divergence projections of this operator are also interdependent, similar to the 
+sequence operator. Hence, this operator is not monotonic with \<open>\<sqsubseteq>\<^sub>\<F>\<close>, \<open>\<sqsubseteq>\<^sub>\<D>\<close> and \<open>\<sqsubseteq>\<^sub>\<T>\<close>, but monotonic 
+when their combinations are considered. \<close>
 
-\<close>
-
-(* Besides the monotonicity results on the above \<^csp> operators, 
-we have also proved that for other \<^csp> operators, such as multi-prefix and non-deterministic choice, 
-they are all monotonic with these five refinement orderings. Such theoretical results provide significant indicators 
-for semantics choices when considering specification decomposition. 
-We want to emphasize that this is the first work on such substantial 
-analysis in a formal way, as far as we know. 
-
-%In the literature, these processes are defined in a way that does not distinguish the special event \<open>tick\<close>. To be consistent with the idea that ticks should be distinguished on the semantic level, besides the above
-three processes,
-
-one can directly prove 3 since for both \<open>CHAOS\<close> and \<open>DF\<close>,
-the version with \<open>SKIP\<close> is constructed exactly in the same way from that without \<open>SKIP\<close>. 
-And 4 is obtained based on the projection laws of internal choice \<open>\<sqinter>\<close>.
-Finally, for 5, the difference between \<open>DF\<close> and \<open>RUN\<close> is that the former applies internal choice 
-while the latter with external choice. From the projection laws of both operators, 
-the failure set of \<open>RUN\<close> has more constraints, thus being a subset of that of \<open>DF\<close>, 
-when the divergence set is empty, which is true for both processes. 
-
-*)
-
-subsection*["processes"::tc,main_author="Some(@{docitem ''safouan''}::author)", 
-                            main_author="Some(@{docitem ''lina''}::author)"]
+subsection*["processes"::technical,main_author="Some(@{author ''safouan''}::author)", 
+                            main_author="Some(@{author ''lina''}::author)"]
 \<open>Reference Processes and their Properties\<close>
 text\<open>
 We now present reference processes that exhibit basic behaviors, introduced in  
@@ -549,43 +510,40 @@ Definition*[X6, level="Some 2"]\<open>\<open>DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P
 
 text\<open>In the following, we denote \<open> \<R>\<P> = {DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P, DF, RUN, CHAOS, CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P}\<close>. 
 All five  reference processes are divergence-free.
-%which was done by using a particular lemma \<open>\<D> (\<mu> x. f x) = \<Inter>\<^sub>i\<^sub>\<in>\<^sub>\<nat> \<D> (f\<^sup>i \<bottom>)\<close>.  
+which was proven by using a particular lemma \<open>\<D> (\<mu> x. f x) = \<Inter>\<^sub>i\<^sub>\<in>\<^sub>\<nat> \<D> (f\<^sup>i \<bottom>)\<close>.  
 @{cartouche 
   [display,indent=8] \<open> D (\<PP> UNIV) = {} where \<PP> \<in> \<R>\<P> and UNIV is the set of all events\<close>
 }
 Regarding the failure refinement ordering, the set of failures \<open>\<F> P\<close> for any process \<open>P\<close> is
-a subset of  \<open>\<F> (CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV)\<close>.% and the following lemma was proved: 
-% This proof is performed by induction, based on the failure projection of \<open>STOP\<close> and that of 
-% internal choice.
-
+a subset of  \<open>\<F> (CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV)\<close>.
 
    @{cartouche [display, indent=25] \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<F> P\<close>}
 
-
-\<^noindent> Furthermore, the following 5 relationships were demonstrated from monotonicity results and 
-a denotational proof.  
-%among which 1 and 2 are immediate corollaries, 
-%4 and 5 are directly obtained from our monotonicity results while 3 requires a denotational proof.
-and thanks to transitivity, we can derive other relationships.
+Furthermore, the following 5 relationships were demonstrated from monotonicity results and
+a denotational proof.
+\<close>
 
 
+Corollary*[co1::"corollary", short_name="\<open>Corollaries on reference processes.\<close>",level="Some 2"]
+\<open> \<^hfill> \<^br>  \<^vs>\<open>-0.3cm\<close>
   \<^enum> \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<sqsubseteq>\<^sub>\<F> CHAOS A\<close>
   \<^enum> \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<sqsubseteq>\<^sub>\<F> DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A\<close>  
   \<^enum> \<open>CHAOS A \<sqsubseteq>\<^sub>\<F> DF A\<close>
   \<^enum> \<open>DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<sqsubseteq>\<^sub>\<F> DF A\<close>  
-  \<^enum> \<open>DF A \<sqsubseteq>\<^sub>\<F> RUN A\<close>  
+  \<^enum> \<open>DF A \<sqsubseteq>\<^sub>\<F> RUN A\<close> \<^vs>\<open>0.3cm\<close>
 
+where 1 and 2 are immediate, and where 4 and 5 are directly obtained from our monotonicity 
+results while 3 requires an argument over the denotational space.
+Thanks to transitivity, we can derive other relationships.\<close>          
 
-Last, regarding trace refinement, for any process P, 
+text\<open> Lastly, regarding trace refinement, for any process P, 
 its set of traces \<open>\<T> P\<close> is a subset of  \<open>\<T> (CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV)\<close> and of  \<open>\<T> (DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV)\<close> as well.
 %As we already proved that \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P\<close> covers all failures, 
 %we can immediately infer that it also covers all traces. 
 %The \<open>DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P\<close> case requires a longer denotational proof.
 
-
   \<^enum> \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<T> P\<close>
   \<^enum> \<open>DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<T> P\<close>
-
 \<close>
 
 text\<open> 
@@ -598,32 +556,27 @@ verification. For example, if one wants to establish that a protocol implementat
 a non-deterministic specification \<open>SPEC\<close> it suffices to ask if \<open>IMPL || SPEC\<close> is deadlock-free.
 In this setting, \<open>SPEC\<close> becomes a kind of observer that signals non-conformance of \<open>IMPL\<close> by 
 deadlock.
-% A livelocked system looks similar to a deadlocked one from an external point of view. 
-% However, livelock is sometimes considered as worse since the user may be able to observe the internal 
-% activities and so hope that some output will happen eventually. 
 
 In the literature, deadlock and lifelock are phenomena that are often 
 handled separately. One contribution of our work is establish their precise relationship inside
 the Failure/Divergence Semantics of \<^csp>.\<close>
 
-(* bizarre: Definition* does not work for this single case *)
-text*[X10::"definition", level="Some 2"]\<open> \<open>deadlock\<^sub>-free P \<equiv>  DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<F> P\<close>  \<close>
+Definition*[X10::"definition", level="Some 2"]\<open> \<open>deadlock\<^sub>-free P \<equiv>  DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<F> P\<close>  \<close>
 
-text\<open>\<^noindent> A process \<open>P\<close> is deadlock-free if and only if after any trace \<open>s\<close> without \<open>\<surd>\<close>, the union of \<open>\<surd>\<close> 
+text\<open>\<^noindent> A process \<open>P\<close> is deadlock-free if and only if after any trace \<open>s\<close> without \<open>\<checkmark>\<close>, the union of \<open>\<checkmark>\<close> 
 and all events of \<open>P\<close> can never be a refusal set associated to \<open>s\<close>, which means that \<open>P\<close> cannot 
 be deadlocked after any non-terminating trace.   
 \<close>
 
 Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>", level="Some 2"]
-\<open> \hfill \break \<open>deadlock_free P \<longleftrightarrow> (\<forall>s\<in>\<T> P. tickFree s \<longrightarrow> (s, {\<surd>}\<union>events_of P) \<notin> \<F> P)\<close> \<close>   
+\<open> \<^hfill> \<^br> \<open>deadlock_free P \<longleftrightarrow> (\<forall>s\<in>\<T> P. tickFree s \<longrightarrow> (s, {\<checkmark>}\<union>events_of P) \<notin> \<F> P)\<close> \<close>   
 Definition*[X11, level="Some 2"]\<open>  \<open>livelock\<^sub>-free P \<equiv> \<D> P = {} \<close>   \<close>
 
 text\<open> Recall that all five reference processes are livelock-free. 
 We also have the following lemmas about the 
 livelock-freeness of processes: 
   \<^enum> \<open>livelock\<^sub>-free P \<longleftrightarrow> \<PP> UNIV \<sqsubseteq>\<^sub>\<D> P where \<PP> \<in> \<R>\<P>\<close> 
-  \<^enum> @{cartouche [display]\<open>livelock\<^sub>-free P \<longleftrightarrow> DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<T>\<^sub>\<D> P 
-                    \<longleftrightarrow> CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<T>\<^sub>\<D> P\<close>}
+  \<^enum> \<open>livelock\<^sub>-free P \<longleftrightarrow> DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<T>\<^sub>\<D> P  \<longleftrightarrow> CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<T>\<^sub>\<D> P\<close>
   \<^enum> \<open>livelock\<^sub>-free P \<longleftrightarrow> CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<F>\<^sub>\<D> P\<close> 
 \<close>
 text\<open>
@@ -644,11 +597,11 @@ then it may still be livelock-free. % This makes sense since livelocks are worse
 
 \<close>
 
-section*["advanced"::tc,main_author="Some(@{docitem ''safouan''}::author)",level="Some 3"]
+section*["advanced"::technical,main_author="Some(@{author ''safouan''}::author)",level="Some 3"]
 \<open>Advanced Verification Techniques\<close>
 
 text\<open>
- Based on the refinement framework discussed in @{docitem "newResults"}, we will now
+ Based on the refinement framework discussed in @{technical "newResults"}, we will now
 turn to some more advanced proof principles, tactics and verification techniques. 
 We will demonstrate them on two paradigmatic examples well-known in the \<^csp> literature: 
 The CopyBuffer and Dijkstra's Dining Philosophers. In both cases, we will exploit 
@@ -659,7 +612,7 @@ verification. In the latter case, we present an approach to a verification of a
 architecture, in this case a ring-structure of arbitrary size.
 \<close>
 
-subsection*["illustration"::tc,main_author="Some(@{docitem ''safouan''}::author)", level="Some 3"]
+subsection*["illustration"::technical,main_author="Some(@{author ''safouan''}::author)", level="Some 3"]
 \<open>The General CopyBuffer Example\<close>
 text\<open>
 We consider the paradigmatic copy buffer example @{cite "Hoare:1985:CSP:3921" and "Roscoe:UCS:2010"} 
@@ -707,7 +660,7 @@ of 2 lines proof-script involving the derived algebraic laws of \<^csp>.
 
 After proving that \<open>SYSTEM\<close> implements \<open>COPY\<close> for arbitrary alphabets, we aim to profit from this 
 first established result to check which relations \<open>SYSTEM\<close> has wrt. to the reference processes of 
-@{docitem "processes"}. Thus, we prove that \<open>COPY\<close> is deadlock-free which implies livelock-free, 
+@{technical "processes"}. Thus, we prove that \<open>COPY\<close> is deadlock-free which implies livelock-free, 
 (proof by fixed-induction  similar to \<open>lemma: COPY \<sqsubseteq> SYSTEM\<close>), from which we can immediately infer 
 from transitivity that \<open>SYSTEM\<close> is. Using refinement relations, we killed four birds with one stone 
 as we proved the deadlock-freeness and  the livelock-freeness for both \<open>COPY\<close> and \<open>SYSTEM\<close> processes. 
@@ -724,7 +677,7 @@ corollary deadlock_free COPY
 \<close>
 
 
-subsection*["inductions"::tc,main_author="Some(@{docitem ''safouan''}::author)"]
+subsection*["inductions"::technical,main_author="Some(@{author ''safouan''}::author)"]
 \<open>New Fixed-Point Inductions\<close>
 
 text\<open>
@@ -741,9 +694,8 @@ For this reason, we derived a number of alternative induction schemes (which are
 in the HOLCF library), which are also relevant for our final Dining Philophers example.
 These are essentially adaptions of k-induction schemes applied to domain-theoretic
 setting (so: requiring \<open>f\<close> continuous and \<open>P\<close> admissible; these preconditions are
-skipped here): 
-  \<^item> @{cartouche [display]\<open>... \<Longrightarrow> \<forall>i<k. P (f\<^sup>i \<bottom>) \<Longrightarrow> (\<forall>X. (\<forall>i<k. P (f\<^sup>i X)) \<longrightarrow> P (f\<^sup>k X)) 
-      \<Longrightarrow> P (\<mu>X. f X)\<close>}
+skipped here):\<^vs>\<open>0.2cm\<close> 
+  \<^item> \<open>... \<Longrightarrow> \<forall>i<k. P (f\<^sup>i \<bottom>) \<Longrightarrow> (\<forall>X. (\<forall>i<k. P (f\<^sup>i X)) \<longrightarrow> P (f\<^sup>k X)) \<Longrightarrow> P (\<mu>X. f X)\<close>
   \<^item> \<open>... \<Longrightarrow> \<forall>i<k. P (f\<^sup>i \<bottom>) \<Longrightarrow> (\<forall>X. P X \<longrightarrow> P (f\<^sup>k X)) \<Longrightarrow> P (\<mu>X. f X)\<close>
 
 
@@ -751,10 +703,9 @@ skipped here):
 it reduces the goal size.
 
 Another problem occasionally occurring in refinement proofs happens when the right side term 
-involves more than one  fixed-point  process (\<^eg> \<open>P \<lbrakk>{A}\<rbrakk> Q \<sqsubseteq> S\<close>). In this situation,
+involves more than one  fixed-point  process (\<^eg> \<open>P \<lbrakk>A\<rbrakk> Q \<sqsubseteq> S\<close>). In this situation,
 we need parallel fixed-point inductions. The HOLCF library offers only a basic one:
-  \<^item> @{cartouche [display]\<open>... \<Longrightarrow> P \<bottom> \<bottom> \<Longrightarrow> (\<forall>X Y. P X Y \<Longrightarrow> P (f X) (g Y)) 
-        \<Longrightarrow> P (\<mu>X. f X) (\<mu>X. g X)\<close>}
+  \<^item> \<open>... \<Longrightarrow> P \<bottom> \<bottom> \<Longrightarrow> (\<forall>X Y. P X Y \<Longrightarrow> P (f X) (g Y)) \<Longrightarrow> P (\<mu>X. f X) (\<mu>X. g X)\<close>
 
 
 \<^noindent> This form does not help in cases like in \<open>P \<lbrakk>\<emptyset>\<rbrakk> Q \<sqsubseteq> S\<close> with the interleaving operator on the 
@@ -776,7 +727,7 @@ The astute reader may notice here that if the induction step is weakened (having
 the base steps require enforcement.  
 \<close>
 
-subsection*["norm"::tc,main_author="Some(@{docitem ''safouan''}::author)"]
+subsection*["norm"::technical,main_author="Some(@{author ''safouan''}::author)"]
 \<open>Normalization\<close>
 text\<open>
  Our framework can reason not only over infinite alphabets, but also over processes parameterized
@@ -797,7 +748,7 @@ This normal form is closed under deterministic and  communication operators.
 The advantage of this format is that we can mimick the well-known product automata construction
 for an arbitrary number of synchronized processes under normal form.
 We only show the case of the synchronous product of two processes: \<close>
-text*[T3::"theorem", short_name="\<open>Product Construction\<close>", level="Some 2"]\<open>
+Theorem*[T3, short_name="\<open>Product Construction\<close>", level="Some 2"]\<open>
 Parallel composition translates to normal form:
 @{cartouche [display,indent=5]\<open>(P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>1,\<upsilon>\<^sub>1\<rbrakk> \<sigma>\<^sub>1) || (P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>2,\<upsilon>\<^sub>2\<rbrakk> \<sigma>\<^sub>2) = 
     P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<lambda>(\<sigma>\<^sub>1,\<sigma>\<^sub>2). \<tau>\<^sub>1 \<sigma>\<^sub>1 \<inter> \<tau>\<^sub>2 \<sigma>\<^sub>2 , \<lambda>(\<sigma>\<^sub>1,\<sigma>\<^sub>2).\<lambda>e.(\<upsilon>\<^sub>1 \<sigma>\<^sub>1 e, \<upsilon>\<^sub>2 \<sigma>\<^sub>2 e)\<rbrakk> (\<sigma>\<^sub>1,\<sigma>\<^sub>2)\<close>}
@@ -836,7 +787,7 @@ Summing up, our method consists of four stages:
 
 \<close>
 
-subsection*["dining_philosophers"::tc,main_author="Some(@{docitem ''safouan''}::author)",level="Some 3"]
+subsection*["dining_philosophers"::technical,main_author="Some(@{author ''safouan''}::author)",level="Some 3"]
 \<open>Generalized Dining Philosophers\<close>
 
 text\<open>  The dining philosophers problem is another paradigmatic example in the \<^csp> literature
@@ -928,7 +879,7 @@ for a dozen of philosophers (on a usual machine) due to the exponential combinat
 Furthermore, our proof is fairly stable against modifications like adding non synchronized events like
 thinking or sitting down in contrast to model-checking techniques. \<close>
 
-section*["relatedwork"::tc,main_author="Some(@{docitem ''lina''}::author)",level="Some 3"]
+section*["relatedwork"::technical,main_author="Some(@{author ''lina''}::author)",level="Some 3"]
 \<open>Related work\<close>
 
 text\<open>
@@ -995,7 +946,7 @@ restrictions on the structure of components. None of our paradigmatic examples c
 be automatically proven with any of the discussed SMT techniques without restrictions.
 \<close>
 
-section*["conclusion"::conclusion,main_author="Some(@{docitem ''bu''}::author)"]\<open>Conclusion\<close>
+section*["conclusion"::conclusion,main_author="Some(@{author ''bu''}::author)"]\<open>Conclusion\<close>
 text\<open>We presented a formalisation of the most comprehensive semantic model for \<^csp>, a 'classical' 
 language for the specification and analysis of concurrent systems studied in a rich body of 
 literature. For this purpose, we ported @{cite "tej.ea:corrected:1997"} to a modern version
@@ -1026,10 +977,6 @@ over finite sub-systems with globally infinite systems in a logically safe way.
 subsection*[bib::bibliography]\<open>References\<close>
 
 close_monitor*[this]
-(*
-term\<open>\<longrightarrow>\<close>
-term\<open> demon \<sigma>\<^sub>g\<^sub>l\<^sub>o\<^sub>b\<^sub>a\<^sub>l := \<Sqinter> \<Delta>t \<in> \<real>\<^sub>>\<^sub>0.     ||| i\<in>A. ACTOR i \<sigma>\<^sub>g\<^sub>l\<^sub>o\<^sub>b\<^sub>a\<^sub>l 
-                                   \<lbrakk>S\<rbrakk> sync!\<sigma>\<^sub>g\<^sub>l\<^sub>o\<^sub>b\<^sub>a\<^sub>l\<^sub>' \<longrightarrow> demon \<sigma>\<^sub>g\<^sub>l\<^sub>o\<^sub>b\<^sub>a\<^sub>l\<^sub>'   \<close>
-*)
+
 end
 (*>*) 

Isabelle_DOF-Examples-Extra/CC_ISO15408/PikeOS_study/PikeOS_ST.thy

@@ -1,7 +1,6 @@
 theory PikeOS_ST (*Security Target *)
 
-imports "../../../src/ontologies/CC_v3.1_R5/CC_v3_1_R5"
-        (*  Isabelle_DOF.CC_v3_1_R5 in the future.  *)
+imports "Isabelle_DOF-Ontologies.CC_v3_1_R5"
 
 begin 
 
@@ -18,18 +17,20 @@ text*[pkosstref::st_ref_cls, title="''PikeOS Security Target''", st_version ="(0
  It complies with the Common Criteria for Information Technology Security Evaluation 
  Version 3.1 Revision 4.\<close>
 
+
+
 subsection*[pkossttoerefsubsec::st_ref_cls]\<open>TOE Reference\<close>
 
 text*[pkostoeref::toe_ref_cls, dev_name="''''", toe_name="''PikeOS''",
       toe_version= "(0,3,4)", prod_name="Some ''S3725''"]
-\<open>The @{docitem toe_def} is the operating system PikeOS version 3.4 
+\<open>The @{docitem (unchecked) toeDef} is the operating system PikeOS version 3.4 
    running on the microprocessor family x86 hosting different applications. 
-   The @{docitem toe_def} is referenced as PikeOS 3.4 base
+   The @{docitem (unchecked) toeDef} is referenced as PikeOS 3.4 base
    product build S3725 for Linux and Windows development host with PikeOS 3.4
    Certification Kit build S4250 and PikeOS 3.4 Common Criteria Kit build S4388.\<close>
 
 subsection*[pkossttoeovrvwsubsec::st_ref_cls]\<open> TOE Overview \<close>
-text*[pkosovrw1::toe_ovrw_cls]\<open>The @{definition \<open>toe\<close> } is a special kind of operating 
+text*[pkosovrw1::toe_ovrw_cls]\<open>The @{docitem (unchecked) \<open>toeDef\<close> } is a special kind of operating 
 system, that allows to effectively separate
 different applications running on the same platform from each other. The TOE can host
 user applications that can also be operating systems. User applications can also be
@@ -87,4 +88,4 @@ open_monitor*[PikosSR::SEC_REQ_MNT]
 close_monitor*[PikosSR]
 
 close_monitor*[stpkos]
-end
+end

Isabelle_DOF-Examples-Extra/CC_ISO15408/PikeOS_study/ROOT

@@ -0,0 +1,4 @@
+session "PikeOS_study" = "Isabelle_DOF-Ontologies" +
+  options [document = false]
+  theories
+    "PikeOS_ST"

Isabelle_DOF-Examples-Extra/CC_ISO15408/ROOTS

@@ -0,0 +1 @@
+PikeOS_study

Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/ROOT

@@ -1,14 +1,16 @@
-session "mini_odo" = "Isabelle_DOF" +
+session "mini_odo" = "Isabelle_DOF-Ontologies" +
   options [document = pdf, document_output = "output", document_build = dof]
   sessions 
     "Physical_Quantities"
   theories
     "mini_odo"
+  document_theories
+    "Isabelle_DOF-Ontologies.CENELEC_50128" 
   document_files
+    "dof_session.tex"
     "preamble.tex"
     "root.bib"
     "root.mst"
-    "lstisadof.sty"
     "figures/df-numerics-encshaft.png"
     "figures/odometer.jpeg"
     "figures/three-phase-odo.pdf"

Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/dof_session.tex

@@ -0,0 +1,3 @@
+\input{mini_odo}
+\input{CENELEC_50128}
+

Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/preamble.tex

@@ -13,8 +13,6 @@
 %%   SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
 
 %% This is a placeholder for user-specific configuration and packages.
-\usepackage{listings}
-\usepackage{lstisadof}
 \usepackage{wrapfig}
 \usepackage{paralist}
 \usepackage{numprint}

Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy

@@ -15,12 +15,12 @@
 theory 
   mini_odo
 imports  
-  "Isabelle_DOF.CENELEC_50128" 
+  "Isabelle_DOF-Ontologies.CENELEC_50128" 
   "Isabelle_DOF.technical_report"
   "Physical_Quantities.SI" "Physical_Quantities.SI_Pretty"
 begin
 use_template "scrreprt-modern"
-use_ontology technical_report and CENELEC_50128
+use_ontology technical_report and "Isabelle_DOF-Ontologies.CENELEC_50128"
 declare[[strict_monitor_checking=true]]
 define_shortcut* dof     \<rightleftharpoons> \<open>\dof\<close>
                  isadof  \<rightleftharpoons> \<open>\isadof{}\<close>
@@ -102,13 +102,13 @@ text\<open>
   functioning of the system and for its integration into the system as a whole. In 
   particular, we need to make the following assumptions explicit: \<^vs>\<open>-0.3cm\<close>\<close>
 
-text*["perfect-wheel"::assumption]
+text*["perfect_wheel"::assumption]
 \<open>\<^item> the wheel is perfectly circular with a given, constant radius. \<^vs>\<open>-0.3cm\<close>\<close>
-text*["no-slip"::assumption]
+text*["no_slip"::assumption]
 \<open>\<^item> the slip between the trains wheel and the track negligible. \<^vs>\<open>-0.3cm\<close>\<close>
-text*["constant-teeth-dist"::assumption]
+text*["constant_teeth_dist"::assumption]
 \<open>\<^item>  the distance between all teeth of a wheel is the same and constant, and \<^vs>\<open>-0.3cm\<close>\<close>
-text*["constant-sampling-rate"::assumption]
+text*["constant_sampling_rate"::assumption]
 \<open>\<^item>  the sampling rate of positions is a given constant.\<close>
 
 text\<open>
@@ -126,13 +126,13 @@ text\<open>
 
 subsection\<open>Capturing ``System Architecture.''\<close>
 
-figure*["three-phase"::figure,relative_width="70",src="''figures/three-phase-odo''"]
+figure*["three_phase"::figure,relative_width="70",file_src="''figures/three-phase-odo.pdf''"]
 \<open>An odometer with three sensors \<open>C1\<close>, \<open>C2\<close>, and \<open>C3\<close>.\<close>
 
 text\<open>
   The requirements analysis also contains a document \<^doc_class>\<open>SYSAD\<close> 
   (\<^typ>\<open>system_architecture_description\<close>) that contains technical drawing of the odometer, 
-  a timing diagram  (see \<^figure>\<open>three-phase\<close>), and tables describing the encoding of the position 
+  a timing diagram  (see \<^figure>\<open>three_phase\<close>), and tables describing the encoding of the position 
   for the possible signal transitions of the sensors \<open>C1\<close>, \<open>C2\<close>, and \<open>C3\<close>. 
 \<close>
 
@@ -146,7 +146,7 @@ text\<open>
   sub-system configuration. \<close>
 
 (*<*)
-declare_reference*["df-numerics-encshaft"::figure] 
+declare_reference*["df_numerics_encshaft"::figure] 
 (*>*)
 subsection\<open>Capturing ``Required Performances.''\<close>
 text\<open>
@@ -160,9 +160,9 @@ text\<open>
 
   The requirement analysis document describes the physical environment, the architecture
   of the measuring device, and the required format and precision of the measurements of the odometry
-  function as represented (see @{figure (unchecked) "df-numerics-encshaft"}).\<close>
+  function as represented (see @{figure (unchecked) "df_numerics_encshaft"}).\<close>
 
-figure*["df-numerics-encshaft"::figure,relative_width="76",src="''figures/df-numerics-encshaft''"]
+figure*["df_numerics_encshaft"::figure,relative_width="76",file_src="''figures/df-numerics-encshaft.png''"]
 \<open>Real distance vs. discrete distance vs. shaft-encoder sequence\<close>
 
 
@@ -215,7 +215,7 @@ text\<open>
   concepts such as Cauchy Sequences, limits, differentiability, and a very substantial part of 
   classical Calculus. \<open>SOME\<close> is the Hilbert choice operator from HOL; the definitions of the 
   model parameters admit all possible positive values as uninterpreted constants. Our 
-  \<^assumption>\<open>perfect-wheel\<close> is translated into a calculation of the circumference of the
+  \<^assumption>\<open>perfect_wheel\<close> is translated into a calculation of the circumference of the
   wheel, while \<open>\<delta>s\<^sub>r\<^sub>e\<^sub>s\<close>, the resolution of the odometer, can be calculated 
   from the these parameters. HOL-Analysis permits to formalize the fundamental physical observables:
 \<close>
@@ -628,14 +628,14 @@ text\<open>
 \<close>
 
 text\<open>Examples for declaration of typed doc-classes "assumption" (sic!) and "hypothesis" (sic!!),
-     concepts defined in the underlying ontology @{theory "Isabelle_DOF.CENELEC_50128"}. \<close>
+     concepts defined in the underlying ontology @{theory "Isabelle_DOF-Ontologies.CENELEC_50128"}. \<close>
 text*[ass2::assumption, long_name="Some ''assumption one''"] \<open> The subsystem Y is safe. \<close>
 text*[hyp1::hypothesis] \<open> \<open>P \<noteq> NP\<close> \<close>
   
 text\<open>  
-   A real example fragment fsrom a larger project, declaring a text-element as a
+   A real example fragment from a larger project, declaring a text-element as a
    "safety-related application condition", a concept defined in the 
-   @{theory "Isabelle_DOF.CENELEC_50128"} ontology:\<close>  
+   @{theory "Isabelle_DOF-Ontologies.CENELEC_50128"} ontology:\<close>  
 
 text*[hyp2::hypothesis]\<open>Under the assumption @{assumption \<open>ass2\<close>} we establish the following: ... \<close>
 
@@ -659,8 +659,7 @@ text*[t10::test_result]
 text \<open> Finally some examples of references to doc-items, i.e. text-elements 
        with declared  meta-information and status. \<close> 
 
-text \<open> As established by @{test_result (unchecked) \<open>t10\<close>}, 
-                         @{test_result (define) \<open>t10\<close>} \<close>
+text \<open> As established by @{test_result \<open>t10\<close>}\<close>
 text \<open> the               @{test_result \<open>t10\<close>}                      
        as well as the    @{SRAC \<open>ass122\<close>}\<close>  
 text \<open> represent a justification of the safety related applicability 
@@ -671,7 +670,6 @@ text \<open> due to notational conventions for antiquotations, one may even writ
        "represent a justification of the safety related applicability
         condition \<^SRAC>\<open>ass122\<close> aka exported constraint \<^EC>\<open>ass122\<close>."\<close> 
 
-
 (*<*)   
 end
 (*>*)

Isabelle_DOF-Examples-Extra/ROOTS

@@ -1,3 +1,5 @@
-scholarly_paper
 technical_report
 CENELEC_50128
+cytology
+CC_ISO15408
+beamerx

Isabelle_DOF-Examples-Extra/beamerx/ROOTS

@@ -0,0 +1,2 @@
+poster
+presentation

Isabelle_DOF-Examples-Extra/beamerx/poster/ROOT

@@ -0,0 +1,8 @@
+chapter AFP 
+
+session "poster-example" (AFP) = "Isabelle_DOF-Ontologies" +
+  options [document = pdf, document_output = "output", document_build = dof, timeout = 300]
+  theories
+    "poster"
+  document_files
+    "preamble.tex"

Isabelle_DOF-Examples-Extra/beamerx/poster/document/preamble.tex

@@ -0,0 +1,2 @@
+%% This is a placeholder for user-specific configuration and packages.
+

Isabelle_DOF-Examples-Extra/beamerx/poster/poster.thy

@@ -0,0 +1,39 @@
+(*<*)
+theory "poster"
+  imports "Isabelle_DOF.scholarly_paper"
+ "Isabelle_DOF-Ontologies.document_templates"
+begin
+
+use_template "beamerposter-UNSUPPORTED"
+use_ontology "scholarly_paper"
+(*>*)
+
+title*[tit::title]\<open>Example Presentation\<close>
+                                  
+author*[safouan,email="\<open>example@example.org\<close>",affiliation="\<open>Example Org\<close>"]\<open>Eliza Example\<close>
+
+text\<open>
+    \vfill
+    \begin{block}{\large Fontsizes}
+      \centering
+      {\tiny tiny}\par
+      {\scriptsize scriptsize}\par
+      {\footnotesize footnotesize}\par
+      {\normalsize normalsize}\par
+      {\large large}\par
+      {\Large Large}\par
+      {\LARGE LARGE}\par
+      {\veryHuge veryHuge}\par
+      {\VeryHuge VeryHuge}\par
+      {\VERYHuge VERYHuge}\par
+    \end{block}
+    \vfill
+\<close>
+
+text\<open>
+@{block (title = "\<open>Title\<^sub>t\<^sub>e\<^sub>s\<^sub>t\<close>") "\<open>Block content\<^sub>t\<^sub>e\<^sub>s\<^sub>t\<close>"}
+\<close>
+
+(*<*)
+end 
+(*>*)

Isabelle_DOF-Examples-Extra/beamerx/presentation/ROOT

@@ -0,0 +1,9 @@
+chapter AFP 
+
+session "presentation-example" (AFP) = "Isabelle_DOF-Ontologies" +
+  options [document = pdf, document_output = "output", document_build = dof, timeout = 300]
+  theories
+    "presentation"
+  document_files
+    "preamble.tex"
+    "figures/A.png"

Isabelle_DOF-Examples-Extra/beamerx/presentation/document/preamble.tex

@@ -0,0 +1,2 @@
+%% This is a placeholder for user-specific configuration and packages.
+

Isabelle_DOF-Examples-Extra/beamerx/presentation/presentation.thy

@@ -0,0 +1,69 @@
+(*<*)
+theory "presentation"
+  imports "Isabelle_DOF.scholarly_paper"
+ "Isabelle_DOF-Ontologies.document_templates"
+begin
+
+use_template "beamer-UNSUPPORTED"
+use_ontology "scholarly_paper"
+(*>*)
+
+title*[tit::title]\<open>Example Presentation\<close>
+                                  
+author*[safouan,email="\<open>example@example.org\<close>",affiliation="\<open>Example Org\<close>"]\<open>Eliza Example\<close>
+
+text\<open>
+\begin{frame}
+\frametitle{Example Slide}
+\centering\huge This is an example!
+\end{frame}
+\<close>
+
+
+frame*[test_frame
+    , frametitle = \<open>\<open>\<open>Example Slide\<^sub>t\<^sub>e\<^sub>s\<^sub>t\<close> with items @{thm "HOL.refl"}\<close>\<close>
+    , framesubtitle = "''Subtitle''"]
+\<open>This is an example!
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> and the term encoding the title of this frame is \<^term_>\<open>frametitle @{frame \<open>test_frame\<close>}\<close>\<close>
+
+frame*[test_frame2
+    , frametitle = "''Example Slide''"
+    , framesubtitle = \<open>\<open>\<open>Subtitle\<^sub>t\<^sub>e\<^sub>s\<^sub>t:\<close> the value of \<^term>\<open>(3::int) + 3\<close> is @{value "(3::int) + 3"}\<close>\<close>]
+\<open>Test frame env \<^term>\<open>refl\<close>\<close>
+
+frame*[test_frame3, frametitle = "''A slide with a Figure''"]
+\<open>A figure
+@{figure_content (width=45, caption=\<open>\<open>Figure\<^sub>t\<^sub>e\<^sub>s\<^sub>t\<close> is not the \<^term>\<open>refl\<close> theorem  (@{thm "refl"}).\<close>)
+                 "figures/A.png"}\<close>
+
+frame*[test_frame4
+    , options = "''allowframebreaks''"
+    , frametitle = "''Example Slide with frame break''"
+    , framesubtitle = \<open>\<open>\<open>Subtitle\<^sub>t\<^sub>e\<^sub>s\<^sub>t:\<close> the value of \<^term>\<open>(3::int) + 3\<close> is @{value "(3::int) + 3"}\<close>\<close>]
+\<open>
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> and the term encoding the title of this frame is \<^term_>\<open>frametitle @{frame \<open>test_frame4\<close>}\<close>
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+\<close>
+
+(*<*)
+end 
+(*>*)

Isabelle_DOF-Examples-Extra/cytology/Cytology.thy

@@ -68,7 +68,7 @@ onto_class procaryotic_cells = cell +
 
 onto_class eucaryotic_cells = cell + 
     organelles :: "organelles' list"
-    invariant has_nucleus :: "\<lambda>\<sigma>::eucaryotic_cells. \<exists> org \<in> set (organelles \<sigma>). is\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s org"
+    invariant has_nucleus :: "\<exists> org \<in> set (organelles \<sigma>). is\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s org"
     \<comment> \<open>Cells must have at least one nucleus. However, this should be executable.\<close>
 
 find_theorems (70)name:"eucaryotic_cells"
@@ -78,13 +78,10 @@ value "is\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s (mk\<^sub>n\<^
 
 term \<open>eucaryotic_cells.organelles\<close>
 
-value \<open>(eucaryotic_cells.organelles(eucaryotic_cells.make X Y Z Z Z [] 3 []))\<close>
-
-value \<open>has_nucleus_inv(eucaryotic_cells.make X Y Z Z Z [] 3 [])\<close>
-
-value \<open>has_nucleus_inv(eucaryotic_cells.make X Y Z Z Z [] 3 
-                         [upcast\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s (nucleus.make a b c d [])])\<close>
+value \<open>(eucaryotic_cells.organelles(eucaryotic_cells.make X Y Z Z Z [] []))\<close>
 
+value \<open>has_nucleus_inv(eucaryotic_cells.make X Y Z Z Z [] [])\<close>
 
+value \<open>has_nucleus_inv(eucaryotic_cells.make X Y Z Z Z [] [upcast\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s (nucleus.make a b c )])\<close>
 
 end

Isabelle_DOF-Examples-Extra/cytology/ROOT

@@ -0,0 +1,4 @@
+session "Cytology" = "Isabelle_DOF" +
+  options [document = false]
+  theories
+    "Cytology"

Isabelle_DOF-Examples-Extra/technical_report/ROOTS

@@ -1,2 +1 @@
-Isabelle_DOF-Manual
 TR_my_commented_isabelle

Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/ROOT

@@ -1,5 +1,5 @@
 session "TR_MyCommentedIsabelle" = "Isabelle_DOF" +
-  options [document = pdf, document_output = "output", document_build = dof, quick_and_dirty = true]
+  options [document = pdf, document_output = "output", document_build = dof]
   theories
     "TR_MyCommentedIsabelle"
   document_files

Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy

@@ -79,7 +79,7 @@ text\<open> \<^vs>\<open>-0.5cm\<close>
   maximum of formal content which makes this text re-checkable at each load and easier 
   maintainable. \<close>
 
-figure*[architecture::figure,relative_width="70",src="''figures/isabelle-architecture''"]\<open> 
+figure*[architecture::figure,relative_width="70",file_src="''figures/isabelle-architecture.pdf''"]\<open> 
      The system architecture of Isabelle (left-hand side) and the  asynchronous communication 
      between the Isabelle system and the IDE (right-hand side). \<close>
 
@@ -148,7 +148,7 @@ text\<open> \<open>*\<open>This is a text.\<close>\<close>\<close>
 
 text\<open>and displayed in the Isabelle/jEdit front-end at the sceen by:\<close>
 
-figure*[fig2::figure, relative_width="60", placement="pl_h", src="''figures/text-element''"]
+figure*[fig2::figure, relative_width="60", file_src="''figures/text-element.pdf''"]
         \<open>A text-element as presented in Isabelle/jEdit.\<close>
 
 text\<open>The text-commands, ML-commands (and in principle any other command) can be seen as 
@@ -347,7 +347,7 @@ text\<open>
 \<^item> \<^ML>\<open>Context.proper_subthy : theory * theory -> bool\<close> subcontext test
 \<^item> \<^ML>\<open>Context.Proof: Proof.context -> Context.generic \<close> A constructor embedding local contexts
 \<^item> \<^ML>\<open>Context.proof_of : Context.generic -> Proof.context\<close> the inverse
-\<^item> \<^ML>\<open>Context.theory_name : theory -> string\<close>
+\<^item> \<^ML>\<open>Context.theory_name : {long:bool} -> theory -> string\<close>
 \<^item> \<^ML>\<open>Context.map_theory: (theory -> theory) -> Context.generic -> Context.generic\<close>
 \<close>
 
@@ -358,7 +358,7 @@ text\<open>The structure \<^ML_structure>\<open>Proof_Context\<close> provides a
 \<^item> \<^ML>\<open>  Context.Proof: Proof.context -> Context.generic \<close>
   the path to a generic Context, i.e. a sum-type of global and local contexts
   in order to simplify system interfaces
-\<^item> \<^ML>\<open> Proof_Context.get_global: theory -> string -> Proof.context\<close>
+\<^item> \<^ML>\<open> Proof_Context.get_global: {long:bool} -> theory -> string -> Proof.context\<close>
 \<close>
 
 
@@ -807,18 +807,13 @@ text\<open>  They reflect the Pure logic depicted in a number of presentations s
   Notated as logical inference rules, these operations were presented as follows:
 \<close>
 
-side_by_side_figure*["text-elements"::side_by_side_figure,anchor="''fig-kernel1''",
-                      caption="''Pure Kernel Inference Rules I ''",relative_width="48",
-                      src="''figures/pure-inferences-I''",anchor2="''fig-kernel2''",
-                      caption2="''Pure Kernel Inference Rules II''",relative_width2="47",
-                      src2="''figures/pure-inferences-II''"]\<open>  \<close>
+text*["text_elements"::float, 
+      main_caption="\<open>Kernel Inference Rules.\<close>"]
+\<open>
+@{fig_content (width=48, caption="Pure Kernel Inference Rules I.") "figures/pure-inferences-I.pdf"
+}\<^hfill>@{fig_content (width=47, caption="Pure Kernel Inference Rules II.") "figures/pure-inferences-II.pdf"} 
+\<close>
 
-(*
-figure*[kir1::figure,relative_width="100",src="''figures/pure-inferences-I''"]
-       \<open> Pure Kernel Inference Rules I.\<close>
-figure*[kir2::figure,relative_width="100",src="''figures/pure-inferences-II''"]
-       \<open> Pure Kernel Inference Rules II. \<close>
- *)
 
 text\<open>Note that the transfer rule:
 \[
@@ -891,7 +886,6 @@ datatype thy = Thy of
 \<^item>  \<^ML>\<open>Theory.axiom_space: theory -> Name_Space.T\<close>
 \<^item>  \<^ML>\<open>Theory.all_axioms_of: theory -> (string * term) list\<close>
 \<^item>  \<^ML>\<open>Theory.defs_of: theory -> Defs.T\<close>
-\<^item>  \<^ML>\<open>Theory.join_theory: theory list -> theory\<close>
 \<^item>  \<^ML>\<open>Theory.at_begin: (theory -> theory option) -> theory -> theory\<close>
 \<^item>  \<^ML>\<open>Theory.at_end: (theory -> theory option) -> theory -> theory\<close>
 \<^item>  \<^ML>\<open>Theory.begin_theory: string * Position.T -> theory list -> theory\<close>
@@ -1144,8 +1138,7 @@ text\<open>
    necessary infrastructure ---  i.e. the operations to pack and unpack theories and
    queries  on it:
 
-\<^item> \<^ML>\<open> Toplevel.theory_toplevel: theory -> Toplevel.state\<close>
-\<^item> \<^ML>\<open> Toplevel.init_toplevel: unit -> Toplevel.state\<close>
+\<^item> \<^ML>\<open> Toplevel.make_state: theory option -> Toplevel.state\<close>
 \<^item> \<^ML>\<open> Toplevel.is_toplevel: Toplevel.state -> bool\<close>
 \<^item> \<^ML>\<open> Toplevel.is_theory: Toplevel.state -> bool\<close>
 \<^item> \<^ML>\<open> Toplevel.is_proof: Toplevel.state -> bool\<close>
@@ -1183,7 +1176,7 @@ text\<open> The extensibility of Isabelle as a system framework depends on a num
  \<^item> \<^ML>\<open>Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition\<close>
    adjoins a theory transformer.
  \<^item> \<^ML>\<open>Toplevel.generic_theory: (generic_theory -> generic_theory) -> Toplevel.transition -> Toplevel.transition\<close>
- \<^item> \<^ML>\<open>Toplevel.theory': (bool -> theory -> theory) -> Toplevel.presentation -> Toplevel.transition -> Toplevel.transition\<close>
+ \<^item> \<^ML>\<open>Toplevel.theory': (bool -> theory -> theory) -> Toplevel.presentation option -> Toplevel.transition -> Toplevel.transition\<close>
  \<^item> \<^ML>\<open>Toplevel.exit: Toplevel.transition -> Toplevel.transition\<close>
  \<^item> \<^ML>\<open>Toplevel.ignored: Position.T -> Toplevel.transition\<close>
  \<^item> \<^ML>\<open>Toplevel.present_local_theory:  (xstring * Position.T) option ->
@@ -1201,7 +1194,6 @@ text\<open>
  \<^item>  \<^ML>\<open>Document.state : unit -> Document.state\<close>, giving the state as a "collection" of named
      nodes, each consisting of an editable list of commands, associated with asynchronous 
      execution process,
- \<^item>  \<^ML>\<open>Session.get_keywords : unit -> Keyword.keywords\<close>, this looks to be session global,
  \<^item>  \<^ML>\<open>Thy_Header.get_keywords : theory -> Keyword.keywords\<close> this looks to be just theory global.
 
 
@@ -1275,7 +1267,6 @@ subsection\<open>Miscellaneous\<close>
 
 text\<open>Here are a few queries relevant for the global config of the isar engine:\<close>
 ML\<open> Document.state();\<close>
-ML\<open> Session.get_keywords(); (* this looks to be  session global. *) \<close>
 ML\<open> Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \<close>
 
   
@@ -1440,7 +1431,7 @@ text\<open>The document model forsees a number of text files, which are organize
   secondary formats can be \<^verbatim>\<open>.sty\<close>,\<^verbatim>\<open>.tex\<close>, \<^verbatim>\<open>.png\<close>, \<^verbatim>\<open>.pdf\<close>, or other files processed 
   by Isabelle and listed in a configuration processed by the build system.\<close>
 
-figure*[fig3::figure, relative_width="100",src="''figures/document-model''"]
+figure*[fig3::figure, relative_width="100",file_src="''figures/document-model.pdf''"]
         \<open>A Theory-Graph in the Document Model\<close>
 
 text\<open>A \<^verbatim>\<open>.thy\<close> file consists of a \<^emph>\<open>header\<close>, a \<^emph>\<open>context-definition\<close> and
@@ -1535,7 +1526,7 @@ text\<open> ... uses the antiquotation @{ML "@{here}"} to infer from the system
   of itself in the global document, converts it to markup (a string-representation of it) and sends
   it via the usual @{ML "writeln"} to the interface. \<close>
 
-figure*[hyplinkout::figure,relative_width="40",src="''figures/markup-demo''"]
+figure*[hyplinkout::figure,relative_width="40",file_src="''figures/markup-demo.png''"]
 \<open>Output with hyperlinked position.\<close>
 
 text\<open>@{figure \<open>hyplinkout\<close>} shows the produced output where the little house-like symbol in the 
@@ -1637,7 +1628,7 @@ val data = \<comment> \<open>Derived from Yakoub's example ;-)\<close>
   , (\<open>Frédéric II\<close>,   \<open>King of Sicily\<close>)
   , (\<open>Frédéric III\<close>,  \<open>the Handsome\<close>)
   , (\<open>Frédéric IV\<close>,   \<open>of the Empty Pockets\<close>)
-  , (\<open>Frédéric V\<close>,    \<open>King of Denmark–Norway\<close>)
+  , (\<open>Frédéric V\<close>,    \<open>King of Denmark-Norway\<close>)
   , (\<open>Frédéric VI\<close>,   \<open>the Knight\<close>)
   , (\<open>Frédéric VII\<close>,  \<open>Count of Toggenburg\<close>)
   , (\<open>Frédéric VIII\<close>, \<open>Count of Zollern\<close>)
@@ -1882,18 +1873,17 @@ Common Stuff related to Inner Syntax Parsing
 \<^item>\<^ML>\<open>Args.internal_typ : typ parser\<close>
 \<^item>\<^ML>\<open>Args.internal_term: term parser\<close>
 \<^item>\<^ML>\<open>Args.internal_fact: thm list parser\<close>
-\<^item>\<^ML>\<open>Args.internal_attribute: (morphism -> attribute) parser\<close>
-\<^item>\<^ML>\<open>Args.internal_declaration: declaration parser\<close>
+\<^item>\<^ML>\<open>Args.internal_attribute: attribute Morphism.entity parser\<close>
 \<^item>\<^ML>\<open>Args.alt_name    : string parser\<close>
 \<^item>\<^ML>\<open>Args.liberal_name: string parser\<close>
 
 
-
 Common Isar Syntax
 \<^item>\<^ML>\<open>Args.named_source: (Token.T -> Token.src) -> Token.src parser\<close>
 \<^item>\<^ML>\<open>Args.named_typ   : (string -> typ) -> typ parser\<close>
 \<^item>\<^ML>\<open>Args.named_term : (string -> term) -> term parser\<close>
-\<^item>\<^ML>\<open>Args.embedded_declaration: (Input.source -> declaration) -> declaration parser\<close>
+\<^item>\<^ML>\<open>Args.embedded_declaration: (Input.source -> Morphism.declaration_entity) ->
+    Morphism.declaration_entity parser\<close>
 \<^item>\<^ML>\<open>Args.typ_abbrev  : typ context_parser\<close>
 \<^item>\<^ML>\<open>Args.typ: typ context_parser\<close>
 \<^item>\<^ML>\<open>Args.term: term context_parser\<close>
@@ -2153,7 +2143,7 @@ text\<open>
 \<^item>\<^ML>\<open>Document_Output.output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text \<close>
 \<^item>\<^ML>\<open>Document_Output.output_token: Proof.context -> Token.T -> Latex.text \<close>
 \<^item>\<^ML>\<open>Document_Output.output_source: Proof.context -> string -> Latex.text \<close>
-\<^item>\<^ML>\<open>Document_Output.present_thy: Options.T -> theory -> Document_Output.segment list -> Latex.text \<close>
+\<^item>\<^ML>\<open>Document_Output.present_thy: Options.T -> Keyword.keywords -> string -> Document_Output.segment list -> Latex.text \<close>
 
 \<^item>\<^ML>\<open>Document_Output.isabelle: Proof.context -> Latex.text  -> Latex.text\<close>
 \<^item>\<^ML>\<open>Document_Output.isabelle_typewriter: Proof.context -> Latex.text  -> Latex.text\<close>

Isabelle_DOF-Examples-Templates/ROOTS

@@ -0,0 +1,9 @@
+template-beamerposter-UNSUPPORTED
+template-beamer-UNSUPPORTED
+template-lipics-v2021-UNSUPPORTED
+template-lncs
+template-scrartcl
+template-scrreprt
+template-scrreprt-modern
+template-sn-article-UNSUPPORTED
+template-svjour3-UNSUPPORTED

Isabelle_DOF-Examples-Templates/template-beamer-UNSUPPORTED/ROOT

@@ -0,0 +1,9 @@
+session "template-beamer-UNSUPPORTED" = "Isabelle_DOF-Ontologies" +
+  options [document = pdf, document_output = "output", document_build = dof]
+(*theories [document = false]
+    A
+    B*)
+  theories
+    "template-beamer-UNSUPPORTED"
+  document_files
+    "preamble.tex"

Isabelle_DOF-Examples-Templates/template-beamer-UNSUPPORTED/document/preamble.tex

@@ -0,0 +1 @@
+%% This is a placeholder for user-specific configuration and packages.

Isabelle_DOF-Examples-Templates/template-beamer-UNSUPPORTED/template-beamer-UNSUPPORTED.thy

@@ -0,0 +1,72 @@
+(*<*)
+theory
+  "template-beamer-UNSUPPORTED"
+imports
+  "Isabelle_DOF-Ontologies.document_templates"
+   Isabelle_DOF.scholarly_paper
+begin
+
+list_templates
+use_template "beamer-UNSUPPORTED"
+list_ontologies
+use_ontology "scholarly_paper"
+(*>*)
+
+title* [tit::title]\<open>Formal Verification of Security Protocols\<close>
+author*[alice, email       = "\<open>alice@example.com\<close>",
+               affiliation = "\<open>Wonderland University\<close>"]\<open>Alice\<close>  
+(* 
+author*[bob,   email       = "\<open>bob@example.com\<close>",
+               affiliation = "\<open>Wonderland University\<close>"]\<open>Bob\<close>  
+*)
+
+text\<open>
+\begin{frame}
+\frametitle{Example Slide}
+\centering\huge This is an example!
+\end{frame}
+\<close>
+
+
+frame*[test_frame
+    , frametitle = \<open>\<open>\<open>Example Slide\<^sub>t\<^sub>e\<^sub>s\<^sub>t\<close> with items @{thm "HOL.refl"}\<close>\<close>
+    , framesubtitle = "''Subtitle''"]
+\<open>This is an example!
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> and the term encoding the title of this frame is \<^term_>\<open>frametitle @{frame \<open>test_frame\<close>}\<close>\<close>
+
+frame*[test_frame2
+    , frametitle = "''Example Slide''"
+    , framesubtitle = \<open>\<open>\<open>Subtitle\<^sub>t\<^sub>e\<^sub>s\<^sub>t:\<close> the value of \<^term>\<open>(3::int) + 3\<close> is @{value "(3::int) + 3"}\<close>\<close>]
+\<open>Test frame env \<^term>\<open>refl\<close>\<close>
+
+frame*[test_frame3
+    , options = "''allowframebreaks''"
+    , frametitle = "''Example Slide with frame break''"
+    , framesubtitle = \<open>\<open>\<open>Subtitle\<^sub>t\<^sub>e\<^sub>s\<^sub>t:\<close> the value of \<^term>\<open>(3::int) + 3\<close> is @{value "(3::int) + 3"}\<close>\<close>]
+\<open>
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> and the term encoding the title of this frame is \<^term_>\<open>frametitle @{frame \<open>test_frame3\<close>}\<close>
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> The term \<^term>\<open>refl\<close> is...
+\<close>
+
+(*<*)
+end 
+(*>*)

Isabelle_DOF-Examples-Templates/template-beamerposter-UNSUPPORTED/ROOT

@@ -0,0 +1,9 @@
+session "template-beamerposter-UNSUPPORTED" = "Isabelle_DOF-Ontologies" +
+  options [document = pdf, document_output = "output", document_build = dof]
+(*theories [document = false]
+    A
+    B*)
+  theories
+    "template-beamerposter-UNSUPPORTED"
+  document_files
+    "preamble.tex"

Isabelle_DOF-Examples-Templates/template-beamerposter-UNSUPPORTED/document/preamble.tex

@@ -0,0 +1 @@
+%% This is a placeholder for user-specific configuration and packages.

Isabelle_DOF-Examples-Templates/template-beamerposter-UNSUPPORTED/template-beamerposter-UNSUPPORTED.thy

@@ -0,0 +1,21 @@
+theory
+  "template-beamerposter-UNSUPPORTED"
+imports
+  "Isabelle_DOF-Ontologies.document_templates"
+   Isabelle_DOF.scholarly_paper
+begin
+
+list_templates
+use_template "beamerposter-UNSUPPORTED"
+list_ontologies
+use_ontology "scholarly_paper"
+
+title* [tit::title]\<open>Formal Verification of Security Protocols\<close>
+author*[alice, email       = "\<open>alice@example.com\<close>",
+               http_site   = "\<open>https://example.com/alice\<close>",
+               affiliation = "\<open>Wonderland University\<close>"]\<open>Alice\<close>  
+author*[bob,   email       = "\<open>bob@example.com\<close>",
+               http_site   = "\<open>https://example.com/bob\<close>",
+               affiliation = "\<open>Wonderland University\<close>"]\<open>Bob\<close>  
+
+end

Isabelle_DOF-Examples-Templates/template-lipics-v2021-UNSUPPORTED/ROOT

@@ -0,0 +1,10 @@
+session "template-lipics-v2021-UNSUPPORTED" = "Isabelle_DOF-Ontologies" +
+  options [document = pdf, document_output = "output", document_build = dof]
+(*theories [document = false]
+    A
+    B*)
+  theories
+    "template-lipics-v2021-UNSUPPORTED"
+  document_files
+    "preamble.tex"
+    "lipics-v2021.cls"

Isabelle_DOF-Examples-Templates/template-lipics-v2021-UNSUPPORTED/document/preamble.tex

@@ -0,0 +1 @@
+%% This is a placeholder for user-specific configuration and packages.

Isabelle_DOF-Examples-Templates/template-lipics-v2021-UNSUPPORTED/template-lipics-v2021-UNSUPPORTED.thy

@@ -0,0 +1,21 @@
+theory
+  "template-lipics-v2021-UNSUPPORTED"
+imports
+  "Isabelle_DOF-Ontologies.document_templates"
+   Isabelle_DOF.scholarly_paper
+begin
+
+list_templates
+use_template "lipics-v2021-UNSUPPORTED"
+list_ontologies
+use_ontology "scholarly_paper"
+
+title* [tit::title]\<open>Formal Verification of Security Protocols\<close>
+author*[alice, email       = "\<open>alice@example.com\<close>",
+               http_site   = "\<open>https://example.com/alice\<close>",
+               affiliation = "\<open>Wonderland University\<close>"]\<open>Alice\<close>  
+author*[bob,   email       = "\<open>bob@example.com\<close>",
+               http_site   = "\<open>https://example.com/bob\<close>",
+               affiliation = "\<open>Wonderland University\<close>"]\<open>Bob\<close>  
+
+end

Isabelle_DOF-Examples-Templates/template-lncs/ROOT

@@ -0,0 +1,9 @@
+session "template-lncs" = "Isabelle_DOF-Ontologies" +
+  options [document = pdf, document_output = "output", document_build = dof]
+(*theories [document = false]
+    A
+    B*)
+  theories
+    "template-lncs"
+  document_files
+    "preamble.tex"

Isabelle_DOF-Examples-Templates/template-lncs/document/preamble.tex

@@ -0,0 +1 @@
+%% This is a placeholder for user-specific configuration and packages.

Isabelle_DOF-Examples-Templates/template-lncs/template-lncs.thy

@@ -0,0 +1,21 @@
+theory
+  "template-lncs"
+imports
+  "Isabelle_DOF-Ontologies.document_templates"
+   Isabelle_DOF.scholarly_paper
+begin
+
+list_templates
+use_template "lncs"
+list_ontologies
+use_ontology "scholarly_paper"
+
+title* [tit::title]\<open>Formal Verification of Security Protocols\<close>
+author*[alice, email       = "\<open>alice@example.com\<close>",
+               http_site   = "\<open>https://example.com/alice\<close>",
+               affiliation = "\<open>Wonderland University\<close>"]\<open>Alice\<close>  
+author*[bob,   email       = "\<open>bob@example.com\<close>",
+               http_site   = "\<open>https://example.com/bob\<close>",
+               affiliation = "\<open>Wonderland University\<close>"]\<open>Bob\<close>  
+
+end

Isabelle_DOF-Examples-Templates/template-scrartcl/ROOT

@@ -0,0 +1,9 @@
+session "template-scrartcl" = "Isabelle_DOF-Ontologies" +
+  options [document = pdf, document_output = "output", document_build = dof]
+(*theories [document = false]
+    A
+    B*)
+  theories
+    "template-scrartcl"
+  document_files
+    "preamble.tex"

Isabelle_DOF-Examples-Templates/template-scrartcl/document/preamble.tex

@@ -0,0 +1 @@
+%% This is a placeholder for user-specific configuration and packages.

Isabelle_DOF-Examples-Templates/template-scrartcl/template-scrartcl.thy

@@ -0,0 +1,21 @@
+theory
+  "template-scrartcl"
+imports
+  "Isabelle_DOF-Ontologies.document_templates"
+   Isabelle_DOF.scholarly_paper
+begin
+
+list_templates
+use_template "scrartcl"
+list_ontologies
+use_ontology "scholarly_paper"
+
+title* [tit::title]\<open>Formal Verification of Security Protocols\<close>
+author*[alice, email       = "\<open>alice@example.com\<close>",
+               http_site   = "\<open>https://example.com/alice\<close>",
+               affiliation = "\<open>Wonderland University\<close>"]\<open>Alice\<close>  
+author*[bob,   email       = "\<open>bob@example.com\<close>",
+               http_site   = "\<open>https://example.com/bob\<close>",
+               affiliation = "\<open>Wonderland University\<close>"]\<open>Bob\<close>  
+
+end

Isabelle_DOF-Examples-Templates/template-scrreprt-modern/ROOT

@@ -0,0 +1,9 @@
+session "template-scrreprt-modern" = "Isabelle_DOF-Ontologies" +
+  options [document = pdf, document_output = "output", document_build = dof]
+(*theories [document = false]
+    A
+    B*)
+  theories
+    "template-scrreprt-modern"
+  document_files
+    "preamble.tex"

Isabelle_DOF-Examples-Templates/template-scrreprt-modern/document/preamble.tex

@@ -0,0 +1 @@
+%% This is a placeholder for user-specific configuration and packages.

Isabelle_DOF-Examples-Templates/template-scrreprt-modern/template-scrreprt-modern.thy

@@ -0,0 +1,21 @@
+theory
+  "template-scrreprt-modern"
+imports
+  "Isabelle_DOF-Ontologies.document_templates"
+   Isabelle_DOF.technical_report
+begin
+
+list_templates
+use_template "scrreprt-modern"
+list_ontologies
+use_ontology "technical_report"
+
+title* [tit::title]\<open>Formal Verification of Security Protocols\<close>
+author*[alice, email       = "\<open>alice@example.com\<close>",
+               http_site   = "\<open>https://example.com/alice\<close>",
+               affiliation = "\<open>Wonderland University\<close>"]\<open>Alice\<close>  
+author*[bob,   email       = "\<open>bob@example.com\<close>",
+               http_site   = "\<open>https://example.com/bob\<close>",
+               affiliation = "\<open>Wonderland University\<close>"]\<open>Bob\<close>  
+
+end

Isabelle_DOF-Examples-Templates/template-scrreprt/ROOT

@@ -0,0 +1,9 @@
+session "template-scrreprt" = "Isabelle_DOF-Ontologies" +
+  options [document = pdf, document_output = "output", document_build = dof]
+(*theories [document = false]
+    A
+    B*)
+  theories
+    "template-scrreprt"
+  document_files
+    "preamble.tex"

Isabelle_DOF-Examples-Templates/template-scrreprt/document/preamble.tex

@@ -0,0 +1 @@
+%% This is a placeholder for user-specific configuration and packages.

Isabelle_DOF-Examples-Templates/template-scrreprt/template-scrreprt.thy

@@ -0,0 +1,21 @@
+theory
+  "template-scrreprt"
+imports
+  "Isabelle_DOF-Ontologies.document_templates"
+   Isabelle_DOF.technical_report
+begin
+
+list_templates
+use_template "scrreprt"
+list_ontologies
+use_ontology "technical_report"
+
+title* [tit::title]\<open>Formal Verification of Security Protocols\<close>
+author*[alice, email       = "\<open>alice@example.com\<close>",
+               http_site   = "\<open>https://example.com/alice\<close>",
+               affiliation = "\<open>Wonderland University\<close>"]\<open>Alice\<close>  
+author*[bob,   email       = "\<open>bob@example.com\<close>",
+               http_site   = "\<open>https://example.com/bob\<close>",
+               affiliation = "\<open>Wonderland University\<close>"]\<open>Bob\<close>  
+
+end

Isabelle_DOF-Examples-Templates/template-sn-article-UNSUPPORTED/ROOT

@@ -0,0 +1,10 @@
+session "template-sn-article-UNSUPPORTED" = "Isabelle_DOF-Ontologies" +
+  options [document = pdf, document_output = "output", document_build = dof]
+(*theories [document = false]
+    A
+    B*)
+  theories
+    "template-sn-article-UNSUPPORTED"
+  document_files
+    "preamble.tex"
+    "sn-jnl.cls"

Isabelle_DOF-Examples-Templates/template-sn-article-UNSUPPORTED/document/preamble.tex

@@ -0,0 +1 @@
+%% This is a placeholder for user-specific configuration and packages.

Isabelle_DOF-Examples-Templates/template-sn-article-UNSUPPORTED/template-sn-article-UNSUPPORTED.thy

@@ -0,0 +1,21 @@
+theory
+  "template-sn-article-UNSUPPORTED"
+imports
+  "Isabelle_DOF-Ontologies.document_templates"
+   Isabelle_DOF.scholarly_paper
+begin
+
+list_templates
+use_template "sn-article-UNSUPPORTED"
+list_ontologies
+use_ontology "scholarly_paper"
+
+title* [tit::title]\<open>Formal Verification of Security Protocols\<close>
+author*[alice, email       = "\<open>alice@example.com\<close>",
+               http_site   = "\<open>https://example.com/alice\<close>",
+               affiliation = "\<open>Wonderland University\<close>"]\<open>Alice\<close>  
+author*[bob,   email       = "\<open>bob@example.com\<close>",
+               http_site   = "\<open>https://example.com/bob\<close>",
+               affiliation = "\<open>Wonderland University\<close>"]\<open>Bob\<close>  
+
+end

Isabelle_DOF-Examples-Templates/template-svjour3-UNSUPPORTED/ROOT

@@ -0,0 +1,11 @@
+session "template-svjour3-UNSUPPORTED" = "Isabelle_DOF-Ontologies" +
+  options [document = pdf, document_output = "output", document_build = dof]
+(*theories [document = false]
+    A
+    B*)
+  theories
+    "template-svjour3-UNSUPPORTED"
+  document_files
+    "preamble.tex"
+    "svjour3.cls"
+    "svglov3.clo"

Isabelle_DOF-Examples-Templates/template-svjour3-UNSUPPORTED/document/preamble.tex

@@ -0,0 +1 @@
+%% This is a placeholder for user-specific configuration and packages.

Isabelle_DOF-Examples-Templates/template-svjour3-UNSUPPORTED/document/svglov3.clo

@@ -0,0 +1,101 @@
+% SVJour3 DOCUMENT CLASS OPTION SVGLOV3 -- for standardised journals
+%
+% This is an enhancement for the LaTeX
+% SVJour3 document class for Springer journals
+%
+%%
+%%
+%% \CharacterTable
+%%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+%%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+%%   Digits        \0\1\2\3\4\5\6\7\8\9
+%%   Exclamation   \!     Double quote  \"     Hash (number) \#
+%%   Dollar        \$     Percent       \%     Ampersand     \&
+%%   Acute accent  \'     Left paren    \(     Right paren   \)
+%%   Asterisk      \*     Plus          \+     Comma         \,
+%%   Minus         \-     Point         \.     Solidus       \/
+%%   Colon         \:     Semicolon     \;     Less than     \<
+%%   Equals        \=     Greater than  \>     Question mark \?
+%%   Commercial at \@     Left bracket  \[     Backslash     \\
+%%   Right bracket \]     Circumflex    \^     Underscore    \_
+%%   Grave accent  \`     Left brace    \{     Vertical bar  \|
+%%   Right brace   \}     Tilde         \~}
+\ProvidesFile{svglov3.clo}
+              [2006/02/03 v3.1
+      style option for standardised journals]
+\typeout{SVJour Class option: svglov3.clo for standardised journals}
+\def\validfor{svjour3}
+\ExecuteOptions{final,10pt,runningheads}
+% No size changing allowed, hence a "copy" of size10.clo is included
+\renewcommand\normalsize{%
+\if@twocolumn
+   \@setfontsize\normalsize\@xpt{12.5pt}%
+\else
+   \if@smallext
+      \@setfontsize\normalsize\@xpt\@xiipt
+   \else
+      \@setfontsize\normalsize{9.5pt}{11.5pt}%
+   \fi
+\fi
+   \abovedisplayskip=3 mm plus6pt minus 4pt
+   \belowdisplayskip=3 mm plus6pt minus 4pt
+   \abovedisplayshortskip=0.0 mm plus6pt
+   \belowdisplayshortskip=2 mm plus4pt minus 4pt
+   \let\@listi\@listI}
+\normalsize
+\newcommand\small{%
+\if@twocolumn
+   \@setfontsize\small{8.5pt}\@xpt
+\else
+   \if@smallext
+      \@setfontsize\small\@viiipt{9.5pt}%
+   \else
+      \@setfontsize\small\@viiipt{9.25pt}%
+   \fi
+\fi
+   \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@
+   \abovedisplayshortskip \z@ \@plus2\p@
+   \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@
+   \def\@listi{\leftmargin\leftmargini
+               \parsep 0\p@ \@plus1\p@ \@minus\p@
+               \topsep 4\p@ \@plus2\p@ \@minus4\p@
+               \itemsep0\p@}%
+   \belowdisplayskip \abovedisplayskip
+}
+\let\footnotesize\small
+\newcommand\scriptsize{\@setfontsize\scriptsize\@viipt\@viiipt}
+\newcommand\tiny{\@setfontsize\tiny\@vpt\@vipt}
+\if@twocolumn
+   \newcommand\large{\@setfontsize\large\@xiipt\@xivpt}
+   \newcommand\LARGE{\@setfontsize\LARGE{16pt}{18pt}}
+\else
+   \newcommand\large{\@setfontsize\large\@xipt\@xiipt}
+   \newcommand\LARGE{\@setfontsize\LARGE{13pt}{15pt}}
+\fi
+\newcommand\Large{\@setfontsize\Large\@xivpt{16dd}}
+\newcommand\huge{\@setfontsize\huge\@xxpt{25}}
+\newcommand\Huge{\@setfontsize\Huge\@xxvpt{30}}
+%
+\def\runheadhook{\rlap{\smash{\lower6.5pt\hbox to\textwidth{\hrulefill}}}}
+\if@twocolumn
+\setlength{\textwidth}{17.4cm}
+\setlength{\textheight}{234mm}
+\AtEndOfClass{\setlength\columnsep{6mm}}
+\else
+   \if@smallext
+      \setlength{\textwidth}{11.9cm}
+      \setlength{\textheight}{19.4cm}
+   \else
+      \setlength{\textwidth}{12.2cm}
+      \setlength{\textheight}{19.8cm}
+   \fi
+\fi
+%
+\AtBeginDocument{%
+\@ifundefined{@journalname}
+ {\typeout{Unknown journal: specify \string\journalname\string{%
+<name of your journal>\string} in preambel^^J}}{}}
+%
+\endinput
+%%
+%% End of file `svglov3.clo'.

Isabelle_DOF-Examples-Templates/template-svjour3-UNSUPPORTED/template-svjour3-UNSUPPORTED.thy

@@ -0,0 +1,21 @@
+theory
+  "template-svjour3-UNSUPPORTED"
+imports
+  "Isabelle_DOF-Ontologies.document_templates"
+   Isabelle_DOF.scholarly_paper
+begin
+
+list_templates
+use_template "svjour3-UNSUPPORTED"
+list_ontologies
+use_ontology "scholarly_paper"
+
+title* [tit::title]\<open>Formal Verification of Security Protocols\<close>
+author*[alice, email       = "\<open>alice@example.com\<close>",
+               http_site   = "\<open>https://example.com/alice\<close>",
+               affiliation = "\<open>Wonderland University\<close>"]\<open>Alice\<close>  
+author*[bob,   email       = "\<open>bob@example.com\<close>",
+               http_site   = "\<open>https://example.com/bob\<close>",
+               affiliation = "\<open>Wonderland University\<close>"]\<open>Bob\<close>  
+
+end