Re-added simple Changelog file.

Reference the issue
#10
in a TODO in the DOF manual to remember to update the manual
when the issue is fixed

.ci/Jenkinsfile

@@ -1,27 +0,0 @@
-pipeline {
-    agent any
-
-    stages {
-        stage('Build Docker') {
-            steps {
-                sh 'cp src/patches/thy_output.ML .ci/isabelle4isadof/'
-                sh 'docker build -t logicalhacking:isabelle4dof .ci/isabelle4isadof'
-                sh 'rm -f .ci/isabelle4isadof/thy_output.ML'
-            }
-        }
-        stage('Check Docker') {
-            when { changeset "src/patches/*" } 
-            steps {
-                sh 'cp src/patches/thy_output.ML .ci/isabelle4isadof/'
-                sh 'docker build --no-cache -t logicalhacking:isabelle4dof .ci/isabelle4isadof'
-                sh 'rm -f .ci/isabelle4isadof/thy_output.ML'
-            }
-        }
-        stage('Build Isabelle/DOF') {
-            steps {
-                sh 'find -type d -name "output" -exec rm -rf {} \\; || true'
-                sh 'docker run -v $PWD:/DOF logicalhacking:isabelle4dof  sh -c "cd /DOF && ./install && isabelle build -D ."'
-            } 
-	}
-    }
-} 

.config

@@ -1,8 +1,8 @@
 # Isabelle/DOF Version Information
-DOF_VERSION="Unreleased"    # "Unreleased" for development, semantic version for releases 
-DOF_LATEST_VERSION="1.0.0"    
-DOF_LATEST_ISABELLE="Isabelle2019"    
-DOF_LATEST_DOI="10.5281/zenodo.3370483"
+DOF_VERSION="1.2.0"    # "Unreleased" for development, semantic version for releases 
+DOF_LATEST_VERSION="1.2.0"    
+DOF_LATEST_ISABELLE="Isabelle2021"    
+DOF_LATEST_DOI="10.5281/zenodo.6385695"
 DOF_GENERIC_DOI="10.5281/zenodo.3370482"
 #
 # Isabelle and AFP Configuration

.woodpecker/README.md

@@ -0,0 +1,14 @@
+# Continuous Build and Release Setup
+
+[![status-badge](https://ci.logicalhacking.com/api/badges/Isabelle_DOF/Isabelle_DOF/status.svg)](https://ci.logicalhacking.com/Isabelle_DOF/Isabelle_DOF)
+
+This directory contains the CI configuration for the [Woodpecker CI](https://woodpecker-ci.org/).
+It may also contain additional tools and script that are useful for preparing a release.
+
+## Generated Artifacts
+
+### Latest Build
+
+* [document.pdf](https://artifacts.logicalhacking.com/ci-confidential/Isabelle_DOF/Isabelle_DOF/main/latest/document.pdf)
+* [browser_info](https://artifacts.logicalhacking.com/ci-confidential/Isabelle_DOF/Isabelle_DOF/main/latest/browser_info/Unsorted/Isabelle_DOF/)
+* [aux files](https://artifacts.logicalhacking.com/ci-confidential/Isabelle_DOF/Isabelle_DOF/main/latest/)

.woodpecker/build.yml

@@ -0,0 +1,27 @@
+pipeline:
+  build:
+    image: docker.io/logicalhacking/isabelle2021
+    commands:
+      - export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/
+      - mkdir -p $ARTIFACT_DIR
+      - export `isabelle getenv ISABELLE_HOME_USER`
+      - ./install
+      - isabelle build -D . -o browser_info
+      - cp -r $ISABELLE_HOME_USER/browser_info $ARTIFACT_DIR
+      - cp output/document.pdf $ARTIFACT_DIR
+      - cd $ARTIFACT_DIR
+      - cd ..
+      - ln -s * latest
+  deploy:
+    image: docker.io/drillster/drone-rsync
+    settings:
+      hosts: [ "ci.logicalhacking.com"]
+      port: 22
+      source: .artifacts/$CI_REPO_OWNER/*
+      target: $CI_REPO_OWNER
+      include: [ "**.*"]
+      key:
+        from_secret: artifacts_ssh
+      user: artifacts
+
+      

.woodpecker/isabelle4isadof/Dockerfile

@@ -24,7 +24,7 @@
 #
 # SPDX-License-Identifier: BSD-2-Clause
 
-FROM logicalhacking/lh-docker-isabelle:isabelle2020
+FROM logicalhacking/lh-docker-isabelle:isabelle2021
 
 WORKDIR /home/isabelle
 COPY thy_output.ML /home/isabelle/Isabelle/src/Pure/Thy

.woodpecker/mk_release

@@ -1,6 +1,6 @@
 #!/usr/bin/env bash
-# Copyright (c) 2019The University of Exeter. 
-#               2019 The University of Paris-Saclay. 
+# Copyright (c) 2019-2022 University of Exeter. 
+#               2019 University of Paris-Saclay. 
 #
 # Redistribution and use in source and binary forms, with or without
 # modification, are permitted provided that the following conditions
@@ -107,7 +107,7 @@ build_and_install_manuals()
     echo "  2018-cicm-isabelle_dof-applications       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/.ci $ISADOF_WORK_DIR/.afp 
+    rm -rf $ISADOF_WORK_DIR/.git* $ISADOF_WORK_DIR/.woodpecker $ISADOF_WORK_DIR/.afp 
     if [ -f $ROOTS.backup ]; then
         mv $ROOTS.backup $ROOTS
     fi

CHANGELOG.md

@@ -5,11 +5,7 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/)
 and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.html).
 
-## [Unreleased]
-
-### Added
-
-### Changed
+## 1.2.0 - 2022-03-26
 
 ## 1.1.0 - 2021-03-20
 

LICENSE

@@ -1,6 +1,6 @@
 Copyright (C) 2018-2019 The University of Sheffield
-              2019-2019 The University of Exeter
-              2018-2019 The University of Paris-Saclay
+              2019-2022 The University of Exeter
+              2018-2022 The University of Paris-Saclay
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without

README.md

@@ -2,8 +2,8 @@
 
 Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle.
 Isabelle/DOF allows for both conventional typesetting as well as formal
-development. The manual for [Isabelle/DOF 1.1.0/Isabelle2020 is available 
-online.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.1.0_Isabelle2020.pdf)
+development. The manual for [Isabelle/DOF 1.2.0/Isabelle2021 is available 
+online.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.pdf)
 
 ## Running Isabelle/DOF using Docker
 
@@ -13,7 +13,7 @@ Docker supports X11 application, you can start Isabelle/DOF as follows:
 
 ```console
 foo@bar:~$ docker run -ti --rm -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-unix \ 
-           logicalhacking/isabelle_dof-1.1.0_isabelle2020 isabelle jedit
+           logicalhacking/isabelle_dof-1.2.0_isabelle2021 isabelle jedit
 ```
 
 ## Pre-requisites
@@ -23,9 +23,8 @@ Isabelle/DOF has two major pre-requisites:
 * **Isabelle:** Isabelle/DOF requires [Isabelle 2021](http://isabelle.in.tum.de/website-Isabelle2021/).
   Please download the Isabelle 2021 distribution for your operating
   system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2021/).
-* **LaTeX:** Isabelle/DOF requires a modern TeX-engine supporting the \expanded{}-primitive. This
-  is, for example, included in the [TeX Live 2020](https://www.tug.org/texlive/) (or later)
-  distribution. 
+* **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least 
+  [TeX Live 2021](https://www.tug.org/texlive/) with all available updates applied.
   
 ## Installation
 
@@ -137,6 +136,14 @@ Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
 For releases, signed archives including a PDF version of the Isabelle/DOF manual are
 are available:
 
+* Isabelle/DOF 1.2.0/Isabelle2021
+  * [Isabelle_DOF-1.2.0_Isabelle2021.pdf](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.pdf)
+  * [Isabelle_DOF-1.2.0_Isabelle2021.tar.xz](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.tar.xz)
+  * [Isabelle_DOF-1.2.0_Isabelle2021.tar.xz.asc](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.tar.xz.asc)
+* Isabelle/DOF 1.1.0/Isabelle2021
+  * [Isabelle_DOF-1.1.0_Isabelle2021.pdf](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.1.0_Isabelle2021.pdf)
+  * [Isabelle_DOF-1.1.0_Isabelle2021.tar.xz](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.1.0_Isabelle2021.tar.xz)
+  * [Isabelle_DOF-1.1.0_Isabelle2021.tar.xz.asc](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.1.0_Isabelle2021.tar.xz.asc)
 * Isabelle/DOF 1.1.0/Isabelle2020
   * [Isabelle_DOF-1.1.0_Isabelle2020.pdf](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.1.0_Isabelle2020.pdf)
   * [Isabelle_DOF-1.1.0_Isabelle2020.tar.xz](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.1.0_Isabelle2020.tar.xz)
@@ -181,12 +188,15 @@ SPDX-License-Identifier: BSD-2-Clause
   Computer Science (11724), Springer-Verlag, 2019.
   [doi:10.1007/978-3-030-30446-1_15](https://doi.org/10.1007/978-3-030-30446-1_15).
 
-* Achim D. Brucker, Burkhart Wolff. [Using Ontologies in Formal Developments Targeting Certification]
-  (https://www.brucker.ch/bibliography/download/2019/brucker.ea-ontologies-certification-2019.pdf). In 
+* Achim D. Brucker, Burkhart Wolff. [Using Ontologies in Formal Developments Targeting Certification](https://www.brucker.ch/bibliography/download/2019/brucker.ea-ontologies-certification-2019.pdf). In 
   Integrated Formal Methods (IFM). Lecture Notes in Computer Science (11918). Springer-Verlag 2019.
   [doi:10.1007/978-3-030-34968-4_4](http://dx.doi.org/10.1007/978-3-030-34968-4_4)  
 
-## Master Repository
+* Sergio Bezzecchi, Paolo Crisafulli, Charlotte Pichot, and Burkhart Wolff. [Making Agile Development 
+  Processes fit for V-style Certification Procedures.](https://hal.archives-ouvertes.fr/hal-01702815/document)
+   In ERTS 2018. <https://hal.archives-ouvertes.fr/hal-01702815>
 
-The master git repository for this project is hosted
-<https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF>.
+## Upstream Repository
+
+The upstream git repository, i.e., the single source of truth, for this project is hosted
+at <https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF>.

examples/ROOTS

@@ -1,4 +1,3 @@
 scholarly_paper
 technical_report
-math_exam
 CENELEC_50128

examples/cytology/Cytology.thy

@@ -0,0 +1,90 @@
+theory Cytology
+  imports "Isabelle_DOF.scholarly_paper"
+begin
+
+text\<open>A small example ontology for demonstration purposes.
+     The presentation follows closely: \<^url>\<open>https://www.youtube.com/watch?v=URUJD5NEXC8\<close>.\<close>
+
+
+datatype protein = filaments | motor_proteins | rna | dna |nucleolus
+
+type_synonym desc = "string"
+
+onto_class organelles   =   description :: desc
+
+find_theorems (60) name:"organelles"
+
+term "Cytology.organelles.make"
+
+onto_class ribosomes    = organelles +    description :: desc
+   
+onto_class mytochondria = organelles +    description :: desc
+
+onto_class golgi_apparatus = organelles + description :: desc
+
+onto_class lysosome    = organelles +     description :: desc
+
+text\<open>the control center of the cell:\<close>
+onto_class nucleus = organelles +  
+       description :: desc
+       components  :: "protein list" <= "[nucleolus]" 
+
+(* Not so nice construction to mimick inheritance on types useds in attribute positions. *)
+datatype organelles' = upcast\<^sub>r\<^sub>i\<^sub>b\<^sub>o\<^sub>s\<^sub>o\<^sub>m\<^sub>e\<^sub>s     (get_ribosomes:ribosomes)
+                     | upcast\<^sub>m\<^sub>y\<^sub>t\<^sub>o\<^sub>c\<^sub>h\<^sub>o\<^sub>n\<^sub>d\<^sub>r\<^sub>i\<^sub>a   (get_mytochondria:mytochondria)
+                     | upcast\<^sub>g\<^sub>o\<^sub>l\<^sub>g\<^sub>i\<^sub>_\<^sub>a\<^sub>p\<^sub>p\<^sub>a\<^sub>r\<^sub>a\<^sub>t\<^sub>u\<^sub>s (get_golgi_apparatus: golgi_apparatus)
+                     | upcast\<^sub>l\<^sub>y\<^sub>s\<^sub>o\<^sub>s\<^sub>o\<^sub>m\<^sub>e      (get_lysosome : lysosome)
+                     | upcast\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s       (get_nucleus : nucleus)
+
+fun is\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s where "is\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s (upcast\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s X) = True" | "is\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s ( _) = False"
+(* ... *)
+fun downcast\<^sub>r\<^sub>i\<^sub>b\<^sub>o\<^sub>s\<^sub>o\<^sub>m\<^sub>e\<^sub>s 
+  where "downcast\<^sub>r\<^sub>i\<^sub>b\<^sub>o\<^sub>s\<^sub>o\<^sub>m\<^sub>e\<^sub>s (upcast\<^sub>r\<^sub>i\<^sub>b\<^sub>o\<^sub>s\<^sub>o\<^sub>m\<^sub>e\<^sub>s X) = X" | "downcast\<^sub>r\<^sub>i\<^sub>b\<^sub>o\<^sub>s\<^sub>o\<^sub>m\<^sub>e\<^sub>s _ = undefined"
+fun downcast\<^sub>m\<^sub>y\<^sub>t\<^sub>o\<^sub>c\<^sub>h\<^sub>o\<^sub>n\<^sub>d\<^sub>r\<^sub>i\<^sub>a 
+  where "downcast\<^sub>m\<^sub>y\<^sub>t\<^sub>o\<^sub>c\<^sub>h\<^sub>o\<^sub>n\<^sub>d\<^sub>r\<^sub>i\<^sub>a (upcast\<^sub>m\<^sub>y\<^sub>t\<^sub>o\<^sub>c\<^sub>h\<^sub>o\<^sub>n\<^sub>d\<^sub>r\<^sub>i\<^sub>a X) = X" | "downcast\<^sub>m\<^sub>y\<^sub>t\<^sub>o\<^sub>c\<^sub>h\<^sub>o\<^sub>n\<^sub>d\<^sub>r\<^sub>i\<^sub>a _ = undefined"
+fun downcast\<^sub>g\<^sub>o\<^sub>l\<^sub>g\<^sub>i\<^sub>_\<^sub>a\<^sub>p\<^sub>p\<^sub>a\<^sub>r\<^sub>a\<^sub>t\<^sub>u\<^sub>s 
+  where "downcast\<^sub>g\<^sub>o\<^sub>l\<^sub>g\<^sub>i\<^sub>_\<^sub>a\<^sub>p\<^sub>p\<^sub>a\<^sub>r\<^sub>a\<^sub>t\<^sub>u\<^sub>s (upcast\<^sub>g\<^sub>o\<^sub>l\<^sub>g\<^sub>i\<^sub>_\<^sub>a\<^sub>p\<^sub>p\<^sub>a\<^sub>r\<^sub>a\<^sub>t\<^sub>u\<^sub>s X) = X" | "downcast\<^sub>g\<^sub>o\<^sub>l\<^sub>g\<^sub>i\<^sub>_\<^sub>a\<^sub>p\<^sub>p\<^sub>a\<^sub>r\<^sub>a\<^sub>t\<^sub>u\<^sub>s _ = undefined"
+fun downcast\<^sub>l\<^sub>y\<^sub>s\<^sub>o\<^sub>s\<^sub>o\<^sub>m\<^sub>e 
+  where "downcast\<^sub>l\<^sub>y\<^sub>s\<^sub>o\<^sub>s\<^sub>o\<^sub>m\<^sub>e (upcast\<^sub>l\<^sub>y\<^sub>s\<^sub>o\<^sub>s\<^sub>o\<^sub>m\<^sub>e X) = X" | "downcast\<^sub>l\<^sub>y\<^sub>s\<^sub>o\<^sub>s\<^sub>o\<^sub>m\<^sub>e _ = undefined"
+fun downcast\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s 
+  where "downcast\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s (upcast\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s X) = X" | "downcast\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s _ = undefined"
+
+
+
+
+onto_class cell = 
+    name             :: string
+    membrane         :: desc   <= "\<open>The outer boundary of the cell\<close>"
+    cytoplasm        :: desc   <= "\<open>The liquid in the cell\<close>"
+    cytoskeleton     :: desc   <= "\<open>includes the thread-like microfilaments\<close>"
+    genetic_material :: "protein list" <= "[rna, dna]"
+
+text\<open>Cells are devided into two categories: \<^emph>\<open>procaryotic\<close> cells (unicellular organisms some 
+bacteria) without a substructuring in organelles and \<^emph>\<open>eucaryotic\<close> cells, as occurring in 
+pluricellular organisms\<close>
+
+onto_class procaryotic_cells = cell +
+    name :: string
+
+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"
+    \<comment> \<open>Cells must have at least one nucleus. However, this should be executable.\<close>
+
+find_theorems (70)name:"eucaryotic_cells"
+find_theorems name:has_nucleus
+
+value "is\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s (mk\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s X)"
+
+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>
+
+
+
+end

examples/math_exam/MathExam/MathExam.thy

@@ -1,111 +0,0 @@
-(*************************************************************************
- * Copyright (C) 
- *               2019      The University of Exeter 
- *               2018-2019 The University of Paris-Saclay
- *               2018      The University of Sheffield
- *
- * License:
- *   This program can be redistributed and/or modified under the terms
- *   of the 2-clause BSD-style license.
- *
- *   SPDX-License-Identifier: BSD-2-Clause
- *************************************************************************)
-
-(*<*)
-theory MathExam
-  imports "Isabelle_DOF.math_exam"
-    HOL.Real
-begin
-(*>*)   
-(* open_monitor*[exam::MathExam]  *)
-
-section*[header::Header,examSubject= "[algebra]", 
-            date="''02-05-2018''", timeAllowed="90::int"] \<open>Exam number 1\<close>
-text\<open>
-\begin{itemize}
-\item Use black ink or black ball-point pen. 
-\item Draw diagrams in pencil.
-\item Answer all questions in the spaces provided.
-\end{itemize}
-\<close>
-
-text*[idir::Author, affiliation="''CentraleSupelec''", 
-         email="''idir.aitsadoune@centralesupelec.fr''"]
-        \<open>Idir AIT SADOUNE\<close>
-  
-  
-figure*[figure::figure, spawn_columns=False,
-        relative_width="80", 
-        src="''figures/Polynomialdeg5''"] 
-        \<open>A Polynome.\<close>
-
-
-subsubsection*[exo1 :: Exercise, content="[q1::Task,q2::Task]"]\<open>Exercise 1\<close>
-text\<open>
-Here are the first four lines of a number pattern.
-\begin{itemize}
-\item Line 1 : @{term "1*6 + 2*4 = 2*7"}
-\item Line 2 : @{term "2*7 + 2*5 = 3*8"}
-\item Line 3 : @{term "3*8 + 2*6 = 4*9"}
-\item Line 4 : @{term "4*9 + 2*7 = 5*10"} 
-\end{itemize}
-\<close>
-
-declare [[show_sorts=false]]  
-subsubsection*[exo2 :: Exercise, content="[q1::Task,q2::Task]"]\<open>Exercise 2\<close> 
-  
-text\<open>Find the roots of the polynome:
-@{term "(x^3) - 6 * x^2 + 5 * x + 12"}.
-Note the intermediate steps in the following fields and submit the solution.\<close>
-text\<open>
-\begin{Form}[action={http://your-web-server.com/path/receiveform.cgi}]
-\begin{tabular}{l}
-    From @{term "(x^3) - 6 * x^2 + 5 * x + 12"}  \\\\  
-    \TextField{have 1} \\\\  
-    \TextField{have 2} \\\\  
-    \TextField{have 3} \\\\
-    \TextField{finally show} \\\\
-    \CheckBox[width=1em]{Has the polynomial as many solutions as its degree ? } \\\\
-    \Submit{Submit}\\
-\end{tabular}
-\end{Form}
-\<close>
-
-(* a bit brutal, as long as lemma* does not yet work *)
-(*<*)
-lemma check_polynome :
-  fixes x::real 
-  shows "(x^3) - 6 * x^2 + 5 * x + 12 = (x-4) * (x+1) * (x - 3)"
-        
-proof -
-  have * : "(x-4) * (x+1) * (x - 3) = (x-4) * ((x+1) * (x-3))"
-         by simp
-  have ** : "... = (x-4) * (x^2 - 2*x - 3)"
-    apply(auto simp: right_diff_distrib add.commute semiring_normalization_rules(1)[symmetric])
-    by (simp add: semiring_normalization_rules(29))
-  have *** : "... = x^3 - 6 * x^2 + 5 * x + 12"
-    apply(auto simp: right_diff_distrib left_diff_distrib add.commute semiring_normalization_rules(1)[symmetric])
-    by (simp add: numeral_3_eq_3 semiring_normalization_rules(29))
-  show ?thesis
-    by(simp only: * ** ***)
-qed
-(*>*)
-
-text*[a1::Answer_Formal_Step]\<open>First Step: Fill in term and justification\<close>
-text*[a2::Answer_Formal_Step]\<open>Next Step: Fill in term and justification\<close>
-text*[a3::Answer_Formal_Step]\<open>Next Step: Fill in term and justification\<close>
-text*[a4::Answer_Formal_Step]\<open>Next Step: Fill in term and justification\<close>
-  
-text*[q1::Task, local_grade="oneStar", mark="1::int", type="formal"] 
-\<open>Complete Line 10 :  @{term "10*x + 2*y =  11*16"}\<close>
-
-subsubsection*[exo3 :: Exercise, content="[q1::Task,q2::Task]"]\<open>Exercise 3\<close>  
-
-text*[q2::Task, local_grade="threeStars", mark="3::int", type="formal"] 
-\<open>Prove that  @{term "n*(n+5) + 2*(n+3) "} is always the product of two numbers 
-   with a difference of 5.
-\<close> 
-(* this does not work on the level of the LaTeX output for known restrictions of the Toplevel. *)
-(* close_monitor*[exam :: MathExam] *)
-
-end

examples/math_exam/MathExam/ROOT

@@ -1,10 +0,0 @@
-session "MathExam" = "Isabelle_DOF" +
-  options [document = pdf, document_output = "output"]
-  theories
-    MathExam
-  document_files
-    "preamble.tex"
-    "isadof.cfg"
-    "preamble.tex"
-    "build"
-    "figures/Polynomialdeg5.png"

examples/math_exam/MathExam/document/build

@@ -1,46 +0,0 @@
-#!/usr/bin/env bash
-# Copyright (c) 2018-2019 The University of Sheffield. All rights reserved.
-#               2018 The University of Paris-Saclay. All rights reserved.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions
-# are met:
-# 1. Redistributions of source code must retain the above copyright
-#    notice, this list of conditions and the following disclaimer.
-# 2. Redistributions in binary form must reproduce the above copyright
-#    notice, this list of conditions and the following disclaimer in
-#    the documentation and/or other materials provided with the
-#    distribution.
-# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
-# FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
-# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
-# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
-# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
-# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
-# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
-# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
-# ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
-# POSSIBILITY OF SUCH DAMAGE.
-#
-# SPDX-License-Identifier: BSD-2-Clause
-
-set -e
-if [ ! -f $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh ]; then
-    echo ""
-    echo "Error: Isabelle/DOF not installed"
-    echo "====="
-    echo "This is a Isabelle/DOF project. The document preparation requires"
-    echo "the Isabelle/DOF framework. Please obtain the framework by cloning"
-    echo "the Isabelle/DOF git repository, i.e.: "
-    echo "    git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
-    echo "You can install the framework as follows:"
-    echo "    cd Isabelle_DOF/document-generator"
-    echo "    ./install"
-    echo ""
-    exit 1
-fi
-
-cp $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh .
-source build_lib.sh

examples/math_exam/MathExam/document/isadof.cfg

@@ -1,2 +0,0 @@
-Template: scrartcl
-Ontology: math_exam

examples/math_exam/MathExam/document/preamble.tex

@@ -1,23 +0,0 @@
-%% Copyright (C) 2018 The University of Sheffield
-%%               2018 The University of Paris-Saclay
-%%               2019 The University of Exeter
-%%
-
-%% License:
-%%   This program can be redistributed and/or modified under the terms
-%%   of the LaTeX Project Public License Distributed from CTAN
-%%   archives in directory macros/latex/base/lppl.txt; either
-%%   version 1.3c of the License, or (at your option) any later version.
-%%   OR
-%%   The 2-clause BSD-style license.
-%%
-%%   SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
-%% Copyright (C) 2018 The University of Sheffield
-%%               2018 The University of Paris-Saclay
-%%
-
-%% This is a placeholder for user-specific configuration and packages. 
-
-\title{<TITLE>}
-\author{<AUTHOR>}
-

examples/math_exam/ROOTS

@@ -1 +0,0 @@
-MathExam

examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/root.bib

@@ -108,7 +108,7 @@
   volume        = 2283,
   doi           = {10.1007/3-540-45949-9},
   abstract      = {This book is a self-contained introduction to interactive
-                  proof in higher-order logic (\acs{hol}), using the proof
+                  proof in higher-order logic HOL, using the proof
                   assistant Isabelle2002. It is a tutorial for potential
                   users rather than a monograph for researchers. The book has
                   three parts.
@@ -121,7 +121,7 @@
                   such advanced topics as nested and mutual recursion. 2.
                   Logic and Sets presents a collection of lower-level tactics
                   that you can use to apply rules selectively. It also
-                  describes Isabelle/\acs{hol}'s treatment of sets, functions
+                  describes Isabelle/HOL's treatment of sets, functions
                   and relations and explains how to define sets inductively.
                   One of the examples concerns the theory of model checking,
                   and another is drawn from a classic textbook on formal

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

@@ -1024,6 +1024,10 @@ 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
 (*>*) 

examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy

@@ -1,7 +1,7 @@
 (*************************************************************************
  * Copyright (C) 
- *               2019-2021 The University of Exeter 
- *               2018-2021 The University of Paris-Saclay
+ *               2019-2022 The University of Exeter 
+ *               2018-2022 The University of Paris-Saclay
  *               2018      The University of Sheffield
  *
  * License:
@@ -21,7 +21,7 @@ section\<open>Local Document Setup.\<close>
 text\<open>Introducing document specific abbreviations and macros:\<close>
 
 define_shortcut* dof     \<rightleftharpoons> \<open>\dof\<close>
-                 isadof  \<rightleftharpoons> \<open>\isadof\<close>
+                 isadof  \<rightleftharpoons> \<open>\isadof{}\<close>
 
 define_shortcut* TeXLive \<rightleftharpoons> \<open>\TeXLive\<close>
                  BibTeX  \<rightleftharpoons> \<open>\BibTeX{}\<close> 
@@ -134,9 +134,9 @@ abstract*[abs, keywordlist="[\<open>Ontology\<close>, \<open>Ontological Modelin
   
     It is an unique feature of  \<^isadof>  that ontologies may be used to control
     the link between formal and informal content in documents in a machine
-    checked way. These links can connect both text elements as well as formal
-    modelling elements such as terms, definitions, code  and logical formulas,
-    alltogether \<^emph>\<open>integrated\<close> in a state-of-the-art interactive theorem prover.
+    checked way. These links can connect both text elements and formal
+    modeling elements such as terms, definitions, code  and logical formulas,
+    altogether \<^emph>\<open>integrated\<close> in a state-of-the-art interactive theorem prover.
 
 \<close>
 

examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy

@@ -119,10 +119,17 @@ text\<open>
       G.~Sala{\"u}n, editors, \<^emph>\<open>Software Engineering and Formal Methods (SEFM)\<close>, number 11724 in
       Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019.
       \href{https://doi.org/10.1007/978-3-030-30446-1_15}{10.1007/978-3-030-30446-1\_15}.
-
     \end{quote}
     A \<^BibTeX>-entry is available at: 
     \<^url>\<open>https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelledof-2019\<close>.
+  \<^item> for an application of \<^isadof> in the context of certifications:
+    \begin{quote}\small
+     A.~D. Brucker and B.~Wolff.
+     Using Ontologies in Formal Developments Targeting Certification. 
+     In W. Ahrendt and S. Tarifa, editors. \<^emph>\<open>Integrated Formal Methods (IFM)\<close>, number 11918.
+     Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019.
+     \href{https://doi.org/10.1007/978-3-030-34968-4\_4}.
+    \end{quote}
 \<close>
 subsubsection\<open>Availability\<close>
 text\<open>

examples/technical_report/Isabelle_DOF-Manual/02_Background.thy

@@ -1,7 +1,7 @@
 (*************************************************************************
  * Copyright (C) 
- *               2019-2021 The University of Exeter 
- *               2018-2021 The University of Paris-Saclay
+ *               2019-2022 The University of Exeter 
+ *               2018-2022 The University of Paris-Saclay
  *               2018      The University of Sheffield
  *
  * License:
@@ -26,7 +26,7 @@ figure*[architecture::figure,relative_width="95",src="''figures/isabelle-archite
      the IDE (right-hand side). \<close>
 
 text*[bg::introduction]\<open>
-While Isabelle @{cite "nipkow.ea:isabelle:2002"} is widely perceived as an interactive theorem 
+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 ``\<^emph>\<open>generic system framework of Isabelle/Isar underlying recent versions of Isabelle.  
@@ -37,20 +37,20 @@ with explicit infrastructure for building derivative systems.\<close>''~@{cite "
 
 The current system framework offers moreover the following features:
 \<^item> a build management grouping components into to pre-compiled sessions,
-\<^item> a prover IDE (PIDE) framework~@{cite "wenzel:asynchronous:2014"} with various front-ends 
+\<^item> a prover IDE (PIDE) framework~@{cite "wenzel:asynchronous:2014"} with various front-ends, 
 \<^item> documentation-generation,
 \<^item> code generators for various target languages,
 \<^item> an extensible front-end language Isabelle/Isar, and,
 \<^item> last but not least, an LCF style, generic theorem prover kernel as 
   the most prominent and deeply integrated system component.
-
-
+\<close>
+text\<open>
 The Isabelle system architecture shown in @{docitem \<open>architecture\<close>} comes with many layers, 
 with Standard ML (SML) at the bottom layer as implementation  language. The architecture actually 
-foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure\<^boxed_sml>\<open>Context\<close>. 
+foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure \<^boxed_sml>\<open>Context\<close>. 
 This structure provides a kind of container called \<^emph>\<open>context\<close> providing an identity, an 
 ancestor-list as well as typed, user-defined state for components (plugins) such as \<^isadof>. 
-On top of the latter, the LCF-Kernel, tactics,  automated proof procedures as well as specific 
+On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific 
 support for higher specification constructs were built.\<close>
 
 section*[dof::introduction]\<open>The Document Model Required by \<^dof>\<close>
@@ -70,13 +70,20 @@ declare_reference*["fig:dependency"::text_section]
 
 
 text\<open>
-  We assume a hierarchical document model\<^index>\<open>document model\<close>, \<^ie>, an \<^emph>\<open>integrated\<close> document 
-  consist of a hierarchy \<^emph>\<open>sub-documents\<close>  (files) that can depend acyclically on each other. 
+  The Isabelle Framework is based on a \<^emph>\<open>document-centric view\<close>\<^bindex>\<open>document-centric view\<close> of 
+  a document, treating the input in its integrality as set of (user-programmable) \<^emph>\<open>document element\<close> 
+  that may mutually depend on and link to each other; A \<^emph>\<open>document\<close> in our sense is what is configured in a set of 
+  \<^verbatim>\<open>ROOT\<close>- and \<^verbatim>\<open>ROOTS\<close>-files.
+
+  Isabelle assumes a hierarchical document model\<^index>\<open>document model\<close>, \<^ie>, an \<^emph>\<open>integrated\<close> document 
+  consist of a hierarchy of \<^emph>\<open>sub-documents\<close>  (files); dependencies are restricted to be
+  acyclic at this level. 
   Sub-documents can have different document types in order to capture documentations consisting of 
   documentation, models, proofs, code of various forms and other technical artifacts.  We call the 
   main sub-document type, for historical reasons, \<^emph>\<open>theory\<close>-files.  A theory file\<^bindex>\<open>theory!file\<close>
   consists of a \<^emph>\<open>header\<close>\<^bindex>\<open>header\<close>, a \<^emph>\<open>context definition\<close>\<^index>\<open>context\<close>, and a body 
-  consisting of a sequence of \<^emph>\<open>command\<close>s (see @{figure (unchecked) "fig:dependency"}). Even 
+  consisting of a sequence of document elements called
+  \<^emph>\<open>command\<close>s (see @{figure (unchecked) "fig:dependency"}). Even
   the header consists of a sequence of commands used for introductory text elements not depending on 
   any context. The context-definition contains an \<^boxed_theory_text>\<open>import\<close> and a 
   \<^boxed_theory_text>\<open>keyword\<close> section, for example:
@@ -96,30 +103,43 @@ text\<open> A text-element \<^index>\<open>text-element\<close> may look like th
   @{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>}
-so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in  \<open>\<open> ... \<close>\<close> paranthesis) which 
-contains characters and and a special notation for semantic macros \<^bindex>\<open>semantic macros\<close> 
+... so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in  \<open>\<open> ... \<close>\<close> parenthesis) which 
+contains characters and a special notation for semantic macros \<^bindex>\<open>semantic macros\<close> 
 (here \<^theory_text>\<open>@{term "fac 5"}).\<close>
 \<close>
 
-text\<open>
-  We distinguish fundamentally two different syntactic levels:
-  \<^item> the \<^emph>\<open>outer-syntax\<close>\<^bindex>\<open>syntax!outer\<close>\<^index>\<open>outer syntax|see {syntax, outer}\<close> (\<^ie>, the 
-    syntax for commands) is processed by a lexer-library and parser combinators built on top, and
-  \<^item> the \<^emph>\<open>inner-syntax\<close>\<^bindex>\<open>syntax!inner\<close>\<^index>\<open>inner syntax|see {syntax, inner}\<close> (\<^ie>, the 
-    syntax for \<open>\<lambda>\<close>-terms in HOL) with its own parametric polymorphism type  checking.
+text\<open>While we concentrate in this manual on \<^theory_text>\<open>text\<close>-document elements --- this is the main
+use of \<^dof> in its current stage --- it is important to note that there are actually three
+families of ``ontology aware'' document elements with analogous 
+syntax to standard ones. The difference is a bracket with meta-data of the form:
+@{theory_text [display,indent=5, margin=70] 
+\<open>
+text*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some semi-formal text \<close>
+ML*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some SML code \<close>
+value*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some annotated \<lambda>-term \<close>
+\<close>}
 
+Depending on the family, we will speak about \<^emph>\<open>(formal) text-contexts\<close>,\<^index>\<open>formal text-contexts\<close> 
+\<^emph>\<open>(ML) code-contexts\<close>\<^index>\<open>code-contexts\<close> and \<^emph>\<open>term-contexts\<close>\<^index>\<open>term-contexts\<close> if we refer 
+to sub-elements inside the \<open>\<open>...\<close>\<close> cartouches of these command families. Note that the Isabelle
+framework allows for nesting cartouches that permits to support switching into a different
+context. In general, this has also the effect that the evaluation of antiquotations changes.
+\<^footnote>\<open>In the literature, this concept has been referred to \<open>Cascade-Syntax\<close> and was used in the 
+Centaur-system and is existing in some limited form in some Emacs-implementations these days. \<close>  
+\<close>
+text\<open>
   On the semantic level, we assume a validation process for an integrated document, where the 
   semantics of a command is a transformation \<open>\<theta> \<rightarrow> \<theta>\<close> for some system state \<open>\<theta>\<close>.
-  This document model can be instantiated with outer-syntax commands for common 
-  text elements, \<^eg>, \<^theory_text>\<open>section\<open>...\<close>\<close> or \<^theory_text>\<open>text\<open>...\<close>\<close>.  
-  Thus, users can add informal text to a sub-document using a text command:
+  This document model can be instantiated depending on  the text-code-, or term-contexts.
+  For common text elements, \<^eg>, \<^theory_text>\<open>section\<open>...\<close>\<close> or \<^theory_text>\<open>text\<open>...\<close>\<close>, 
+  users can add informal text to a sub-document using a text command:
   @{boxed_theory_text [display] \<open>text\<open>This is a description.\<close>\<close> }
   This will type-set the corresponding text in, for example, a PDF document.  However, this 
   translation is not necessarily one-to-one: text elements can be enriched by formal, \<^ie>, 
   machine-checked content via \<^emph>\<open>semantic macros\<close>, called antiquotations\<^bindex>\<open>antiquotation\<close>:
   @{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>
+  \<open>text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm "refl"}, we obtain in \<Gamma> 
+         for @{term \<open>fac 5\<close>} the result @{value \<open>fac 5\<close>}.\<close>\<close>
   }
 which is represented in the final document (\<^eg>, a PDF) by:
 @{boxed_pdf [display]
@@ -137,10 +157,12 @@ for $\operatorname{fac} \text{\textrm{5}}$ the result $\text{\textrm{120}}$.\<cl
   typeset. They represent the device for linking the formal with the informal. 
 \<close>
 
+
+
 figure*["fig:dependency"::figure,relative_width="70",src="''figures/document-hierarchy''"]
        \<open>A Theory-Graph in the Document Model. \<close>
 
-section*[bgrnd21::introduction]\<open>Implementability of the Required Document Model\<close>
+section*[bgrnd21::introduction]\<open>Implementability of the Document Model in other ITP's\<close>
 text\<open> 
   Batch-mode checkers for \<^dof> can be implemented in all systems of the LCF-style prover family, 
   \<^ie>, systems with a type-checked \<open>term\<close>, and abstract \<open>thm\<close>-type for theorems 
@@ -166,7 +188,7 @@ text\<open>
 
   Isabelle provides, beyond the features required for \<^dof>, a lot of additional benefits. 
   Besides UTF8-support for characters used in text-elements, Isabelle offers built-in already a 
-  mechanism user-programmable antiquotations \<^index>\<open>antiquotations\<close> which we use to implement
+  mechanism for user-programmable antiquotations \<^index>\<open>antiquotations\<close> which we use to implement
   semantic macros  \<^index>\<open>semantic macros\<close> in \<^isadof> (We will actually use these two terms
   as synonym in the context of \<^isadof>). Moreover, \<^isadof> allows for the asynchronous 
   evaluation and checking of the document content~@{cite "wenzel:asynchronous:2014" and 

examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy

@@ -1,7 +1,7 @@
 (*************************************************************************
  * Copyright (C) 
- *               2019-2021 The University of Exeter 
- *               2018-2021 The University of Paris-Saclay
+ *               2019-2022 The University of Exeter 
+ *               2018-2022 The University of Paris-Saclay
  *               2018      The University of Sheffield
  *
  * License:
@@ -24,13 +24,13 @@ begin
 chapter*[isadof_tour::text_section]\<open>\<^isadof>: A Guided Tour\<close>
 
 text\<open>
-  In this chapter, we will give a introduction into using \<^isadof> for users that want to create and 
+  In this chapter, we will give an introduction into using \<^isadof> for users that want to create and 
   maintain documents following an existing document ontology.
 \<close>
 
 section*[getting_started::technical]\<open>Getting Started\<close>
 text\<open>
-As an alternative to installing \<^isadof>{} locally, the latest official release  \<^isadof> is also 
+As an alternative to installing \<^isadof>{} locally, the latest official release of \<^isadof> is also 
 available on \href{https://cloud.docker.com/u/logicalhacking/}{Docker Hub}. Thus, if you have 
 \href{https://www.docker.com}{Docker} installed and 
 your installation of Docker supports X11 application, you can start \<^isadof> as follows:
@@ -39,6 +39,9 @@ your installation of Docker supports X11 application, you can start \<^isadof> a
    -v /tmp/.X11-unix:/tmp/.X11-unix \ 
    logicalhacking/isabelle_dof-ë\doflatestversionë_ë\MakeLowercase{\isabellelatestversion}ë \
    isabelle jedit\<close>}
+
+Further configuration of the X11 permissions to authorize docker to start \<^isadof> might be required,
+depending on the user system configuration.
 \<close>
 
 subsection*[installation::technical]\<open>Installation\<close>
@@ -47,8 +50,8 @@ text\<open>
   \<^LaTeX>. We assume a basic familiarity with a Linux/Unix-like command line (i.e., a shell). 
 
   \<^isadof> requires Isabelle\<^bindex>\<open>Isabelle\<close> (\isabellefullversion) with a recent \<^LaTeX>-distribution
-  (e.g., Tex Live 2020 or later).    
-  \<^isadof> uses a two-part version system (e.g., 1.0.0/2020),  where the first part is the version
+  (e.g., Tex Live 2021 or later).    
+  \<^isadof> uses a two-part version system (e.g., 1.1.0/Isabelle2021),  where the first part is the version
   of \<^isadof> (using semantic versioning) and the second part is the supported version of Isabelle. 
   Thus, the same version of \<^isadof> might be available for different versions of Isabelle. 
 \<close>
@@ -74,7 +77,7 @@ text\<open>
   Modern Linux distribution will allow you to install \<^TeXLive> using their respective package 
   managers. On a modern Debian system or a Debian derivative (\<^eg>, Ubuntu), the following command 
   should install all required \<^LaTeX> packages:
-@{boxed_bash [display]\<open>ë\prompt{}ë sudo aptitude install texlive-latex-extra texlive-fonts-extra\<close>}
+@{boxed_bash [display]\<open>ë\prompt{}ë sudo aptitude install texlive-full\<close>}
 \<close>
 
 subsubsection*[isadof::technical]\<open>Installing \<^isadof>\<close>
@@ -85,7 +88,7 @@ text\<open>
   We start by extracting the \<^isadof> archive:
 @{boxed_bash [display]\<open>ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë\<close>}
 This will create a directory \texttt{\isadofdirn} containing \<^isadof> distribution.
-Next, we need to invoke the \<^boxed_bash>\<open>install\<close> script. If necessary, the installations 
+Next, we need to invoke the \<^boxed_bash>\<open>install\<close> script. If necessary, the installation 
 automatically downloads additional dependencies from the AFP (\<^url>\<open>https://www.isa-afp.org\<close>), 
 namely the AFP  entries ``Functional Automata''~@{cite "nipkow.ea:functional-Automata-afp:2004"} 
 and ``Regular Sets and Expressions''~@{cite "kraus.ea:regular-sets-afp:2010"}. This might take a 
@@ -138,7 +141,7 @@ Isabelle/DOF Installer
   /usr/local/Isabelleë\isabelleversion/bin/isabelleë build -D . \<close>}
 
 After the successful installation, you can explore the examples (in the sub-directory 
-\<^boxed_bash>\<open>examples\<close> or create your own project. On the first start, the session 
+\<^boxed_bash>\<open>examples\<close>) or create your own project. On the first start, the session 
 \<^boxed_bash>\<open>Isabelle_DOF\<close> will be built automatically. If you want to pre-build this 
 session and all example documents, execute:
 @{boxed_bash [display]\<open>ë\prompt{\isadofdirn}ë isabelle build -D . \<close>} 
@@ -158,13 +161,13 @@ Now use the following coëëmmand line to build the session:
   isabelle build -D myproject \<close>}
   The created project uses the default configuration (the ontology for writing academic papers 
   (scholarly\_paper) using a report layout based on the article class (\<^boxed_latex>\<open>scrartcl\<close>) of 
-  the KOMA-Script bundle~@{cite "kohm:koma-script:2019"}. The directory \<^boxed_bash>\<open>myproject\<close> 
+  the KOMA-Script bundle~@{cite "kohm:koma-script:2019"}). The directory \<^boxed_bash>\<open>myproject\<close> 
   contains the \<^isadof>-setup for your  new document. To check the document formally, including the 
-  generation of the document in PDF, you only need to execute
+  generation of the document in \<^pdf>, you only need to execute
 
-@{boxed_bash [display]\<open>ë\prompt{}ë  isabelle build -d . myproject \<close>}
+@{boxed_bash [display]\<open>ë\prompt{myproject}ë  isabelle build -d . myproject \<close>}
 
-The dictory  \<^boxed_bash>\<open>myproject\<close> contains the following files and directories: 
+The directory  \<^boxed_bash>\<open>myproject\<close> contains the following files and directories: 
 \begin{center}
 \begin{minipage}{.9\textwidth}
 \dirtree{%
@@ -172,7 +175,7 @@ The dictory  \<^boxed_bash>\<open>myproject\<close> contains the following files
 .2 myproject.
 .3 document.
 .4 build\DTcomment{Build Script}.
-.4 isadof.cfg\DTcomment{\<^isadof> configuraiton}.
+.4 isadof.cfg\DTcomment{\<^isadof> configuration}.
 .4 preamble.tex\DTcomment{Manual \<^LaTeX>-configuration}.
 .3 ROOT\DTcomment{Isabelle build-configuration}.
 }
@@ -193,14 +196,14 @@ users are:
 
 text\<open>
   Creating a new document setup requires two decisions:
-  \<^item> which ontologies (\<^eg>, scholarly\_paper) are required and 
+  \<^item> which ontologies (\<^eg>, scholarly\_paper) are required, and 
   \<^item> which document template (layout)\index{document template} should be used 
-    (\<^eg>, scrartcl\index{scrartcl}). Some templates (\<^eg>, lncs) require that the users manually 
-    obtains and adds the necessary \<^LaTeX> class file (\<^eg>, \<^boxed_bash>\<open>llncs.cls\<close>. 
+    (\<^eg>, scrartcl\index{scrartcl}). Some templates require that the users manually 
+    obtains and adds the necessary \<^LaTeX> class file. 
     This is due to licensing restrictions).\<close>
 text\<open> 
-  This can be configured by using the command-line options of of  \<^boxed_bash>\<open>mkroot_DOF\<close>. In 
-  Particular, \<^boxed_bash>\<open>-o\<close> allows selecting the ontology and \<^boxed_bash>\<open>-t\<close> allows to selecting 
+  This can be configured by using the command-line options of \<^boxed_bash>\<open>mkroot_DOF\<close>. In 
+  Particular, \<^boxed_bash>\<open>-o\<close> allows selecting the ontology and \<^boxed_bash>\<open>-t\<close> allows selecting 
   the document template. The built-in help (using  \<^boxed_bash>\<open>-h\<close>) shows all available options 
   as well as a complete list of the available document templates and ontologies: 
 
@@ -228,49 +231,96 @@ Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
 
 \<close>
 
+section*[writing_doc::technical]\<open>Writing Documents: General Remarks\<close>
+
+subsection*[naming::example]\<open>Name-Spaces, Long- and Short-Names\<close>
+text\<open>\<^isadof> is built upon the name space and lexical conventions of Isabelle. Long-names were 
+composed of a name of the session, the name of the theory, and a sequence of local names referring
+to, \<^eg>, nested specification constructs that were used to identify types, constant symbols, 
+definitions, \<^etc>. The general format of a long-name is 
+
+ \<^boxed_theory_text>\<open> session_name.theory_name.local_name. ... .local_name\<close>
+
+By lexical conventions, theory-names must be unique inside a session
+(and session names must be unique too), such that long-names are unique by construction.
+There are actually different name categories that form a proper name space, \<^eg>, the name space for
+constant symbols and type symbols are distinguished.
+
+Isabelle identifies names already with the shortest suffix that is unique in the global 
+context and in the appropriate name category. This also holds for pretty-printing, which can
+at times be confusing since names stemming from the same specification construct may
+be printed with different prefixes according to their uniqueness.
+\<close>
+
+subsection*[cartouches::example]\<open>Caveat: Lexical Conventions of Cartouches, Strings, Names, ... \<close>
+text\<open>WARNING: The embedding of strings, terms, names \<^etc>, as parts of commands, anti-quotations,
+terms,  \<^etc>, is unfortunately not always so consistent as one might expect, when it comes
+to variants that should be lexically equivalent in principle. This can be a nuisance for
+users, but is again a consequence that we build on existing technology that has been developed
+over decades. 
+\<close>
+
+text\<open>At times, this causes idiosyncrasies like the ones cited in the following incomplete list: 
+\<^item> text-antiquotations
+  \<^theory_text>\<open>text\<close>\<^latex>\<open>\isasymopen\textbf{thm} "normally\_behaved\_def"\isasymclose\ \<close>  
+  versus \<^theory_text>\<open>text\<close>\<^latex>\<open>\isasymopen @\{\textbf{thm} "srac$_1$\_def"\}\isasymclose\ \<close>  
+  (while
+  \<^theory_text>\<open>text\<close>\<^latex>\<open>\isasymopen @\{\textbf{thm} \isasymopen srac$_1$\_def \isasymclose\}\isasymclose\ \<close>
+  fails)
+\<^item> commands \<^theory_text>\<open>thm fundamental_theorem_of_calculus\<close> and
+  \<^theory_text>\<open>thm\<close>\<^latex>\<open> "fundamental\_theorem\_of\_calculus"\<close>
+  or \<^theory_text>\<open>lemma\<close> \<^latex>\<open>"H"\<close> and \<^theory_text>\<open>lemma \<open>H\<close>\<close> and  \<^theory_text>\<open>lemma H\<close> 
+\<^item> string expressions  \<^theory_text>\<open>term\<close>\<^latex>\<open>\isasymopen ''abc'' @ ''cd''\isasymclose\ \<close> and equivalent
+  \<^theory_text>\<open>term\<close>\<^latex>\<open>\isasymopen \isasymopen abc\isasymclose\ @ \isasymopen cd\isasymclose\isasymclose\<close>;
+  but 
+  \<^theory_text>\<open>term\<close>\<^latex>\<open>\isasymopen\isasymopen A \isasymlongrightarrow\ B\isasymclose\isasymclose\ \<close>   
+  not equivalent to \<^theory_text>\<open>term\<close>\<^latex>\<open>\isasymopen''A \isasymlongrightarrow\ B''\isasymclose\ \<close>
+  which fails. 
+\<close>
+
 section*[scholar_onto::example]\<open>Writing Academic Publications in \<^boxed_theory_text>\<open>scholarly_paper\<close>\<close>  
 subsection\<open>Writing Academic Papers\<close>
 text\<open> 
-  The ontology \<^boxed_theory_text>\<open>scholarly_paper\<close>
+  The ontology \<^verbatim>\<open>scholarly_paper\<close>
   \<^index>\<open>ontology!scholarly\_paper\<close> is an ontology modeling 
-  academic/scientific papers, with a slight bias to texts in the domain of mathematics and engineering. 
-  We explain first the principles of its underlying ontology, and then we present two ''real'' 
+  academic/scientific papers, with a slight bias towards texts in the domain of mathematics and engineering. 
+  We explain first the principles of its underlying ontology, and then we present two ``real'' 
   examples from our own publication practice.
 \<close>
 text\<open>
   \<^enum> The iFM 2020 paper~@{cite "taha.ea:philosophers:2020"} is a typical mathematical text,
     heavy in definitions with complex  mathematical notation and a lot of non-trivial cross-referencing
-    between statements, definitions and proofs which is ontologically tracked. However, wrt.
+    between statements, definitions and proofs which are ontologically tracked. However, wrt.
     the possible linking between the underlying formal theory and this mathematical presentation,
     it follows a pragmatic path without any ``deep'' linking to types, terms and theorems, 
     deliberately not exploiting \<^isadof> 's full potential with this regard.
   \<^enum> In the CICM 2018 paper~@{cite "brucker.ea:isabelle-ontologies:2018"}, we deliberately
-    refrain from integrating references to formal content in order  demonstrate that \<^isadof> is not 
+    refrain from integrating references to formal content in order to demonstrate that \<^isadof> is not 
     a  framework from Isabelle users to Isabelle users only, but people just avoiding as much as
     possible \<^LaTeX> notation.
 
   The \<^isadof> distribution contains both examples using the ontology \<^verbatim>\<open>scholarly_paper\<close> in 
   the directory \nolinkurl{examples/scholarly_paper/2018-cicm-isabelle_dof-applications/} or
-  \nolinkurl{examples/scholarly_paper/2020-ifm-csp-applications/}.
+  \nolinkurl{examples/scholarly_paper/2020-iFM-CSP}.
 
   You can inspect/edit the example in Isabelle's IDE, by either 
-  \<^item> starting Isabelle/jedit using your graphical user interface (\<^eg>, by clicking on the 
+  \<^item> starting Isabelle/jEdit using your graphical user interface (\<^eg>, by clicking on the 
     Isabelle-Icon provided by the Isabelle installation) and loading the file 
-    \nolinkurl{examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy}.
-  \<^item> starting Isabelle/jedit from the command line by,\<^eg>, calling:
+    \nolinkurl{examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy},
+  \<^item> starting Isabelle/jEdit from the command line by, \<^eg>, calling:
 
 @{boxed_bash [display]\<open>ë\prompt{\isadofdirn}ë 
   isabelle jedit -d . examples/scholarly_paper/2020-iFM-CSP/paper.thy \<close>}
 \<close> 
 
 
-text\<open>    You can build the PDF-document at the command line by calling:
+text\<open>    You can build the \<^pdf>-document at the command line by calling:
 @{boxed_bash [display] \<open>ë\prompt{}ë isabelle build -d . 2020-iFM-csp \<close>}
 \<close>
 
 subsection*[sss::technical]\<open>A Bluffers Guide to the \<^verbatim>\<open>scholarly_paper\<close> Ontology\<close>
 text\<open> In this section we give a minimal overview of the ontology formalized in
-      @{theory \<open>Isabelle_DOF.scholarly_paper\<close>}.\<close>
+      \<^theory>\<open>Isabelle_DOF.scholarly_paper\<close>.\<close>
 
 text\<open>  We start by modeling the usual text-elements of an academic paper: the title and author 
   information, abstract, and text section: 
@@ -292,18 +342,18 @@ doc_class abstract =
    principal_theorems :: "thm list"\<close>}
 \<close>
 
-text\<open>Note \<open>short_title\<close> and \<open>abbrev\<close> are optional and have the default \<open>None\<close> (no value).
-Note further, that abstracts may have a \<open>principal_theorems\<close> list, where the built-in \<^isadof> type
-\<open>thm list\<close> which contain references to formally proven theorems that must exist in the logical
-context of this document; this is a decisive feature of \<^isadof> that conventional ontological
-languages lack.\<close>
+text\<open>Note \<^const>\<open>short_title\<close> and \<^const>\<open>abbrev\<close> are optional and have the default \<^const>\<open>None\<close>
+(no value). Note further, that \<^typ>\<open>abstract\<close>s may have a \<^const>\<open>principal_theorems\<close> list, where
+the built-in \<^isadof> type \<^typ>\<open>thm list\<close> contains references to formally proven theorems that must
+exist in the logical context of this document; this is a decisive feature of \<^isadof> that
+conventional ontological languages lack.\<close>
 
-text\<open>We continue by the introduction of a main class: the text-element \<open>text_section\<close> (in contrast
-to \<open>figure\<close> or \<open>table\<close> or similar). Note that
-the \<open>main_author\<close> is typed with the class \<open>author\<close>, a HOL type that is automatically derived from
-the document class definition \<open>author\<close> shown above. It is used to express which author currently
-``owns'' this \<open>text_section\<close>, an information that can give rise to presentational or even
-access-control features in a suitably adapted front-end.
+text\<open>We continue by the introduction of a main class: the text-element \<^typ>\<open>text_section\<close>
+(in contrast to \<^typ>\<open>figure\<close> or \<open>table\<close> or similar). Note that
+the \<^const>\<open>main_author\<close> is typed with the class \<^typ>\<open>author\<close>, a HOL type that is automatically
+derived from the document class definition \<^typ>\<open>author\<close> shown above. It is used to express which
+author currently ``owns'' this \<^typ>\<open>text_section\<close>, an information that can give rise to
+presentational or even access-control features in a suitably adapted front-end.
  
 @{boxed_theory_text [display] \<open>
 doc_class text_section = text_element +
@@ -312,16 +362,16 @@ doc_class text_section = text_element +
    level       :: "int  option"    <=  "None"
 \<close>}
 
-The \<open>level\<close>-attibute \<^index>\<open>level\<close> enables doc-notation support for headers, chapters, sections, and 
-subsections; we follow here the \<^LaTeX> terminology on levels to which \<^isadof> is currently targeting at.
-The values are interpreted accordingly to the \<^LaTeX> standard. The correspondance between the levels
+The \<^const>\<open>Isa_COL.text_element.level\<close>-attibute \<^index>\<open>level\<close> enables doc-notation support for
+headers, chapters, sections, and subsections; we follow here the \<^LaTeX> terminology on levels to which \<^isadof> is currently targeting at.
+The values are interpreted accordingly to the \<^LaTeX> standard. The correspondence between the levels
 and the structural entities is summarized as follows:
 
-   \<^item> part          \<^index>\<open>part\<close>          \<^bigskip>\<^bigskip>  \<open>Some -1\<close> \vspace{-1cm} 
-   \<^item> chapter       \<^index>\<open>chapter\<close>       \<^bigskip>\<^bigskip>  \<open>Some 0\<close> \vspace{-1cm}
-   \<^item> section       \<^index>\<open>section\<close>       \<^bigskip>\<^bigskip>  \<open>Some 1\<close> \vspace{-1cm}
-   \<^item> subsection    \<^index>\<open>subsection\<close>    \<^bigskip>\<^bigskip>  \<open>Some 2\<close>  \vspace{-1cm}
-   \<^item> subsubsection \<^index>\<open>subsubsection\<close> \<^bigskip>\<^bigskip>  \<open>Some 3\<close>  \vspace{-0.1cm}
+   \<^item> part          \<^index>\<open>part\<close>          \<open>Some -1\<close> \vspace{-0.3cm}
+   \<^item> chapter       \<^index>\<open>chapter\<close>       \<open>Some 0\<close>  \vspace{-0.3cm}
+   \<^item> section       \<^index>\<open>section\<close>       \<open>Some 1\<close>  \vspace{-0.3cm}
+   \<^item> subsection    \<^index>\<open>subsection\<close>    \<open>Some 2\<close>  \vspace{-0.3cm}
+   \<^item> subsubsection \<^index>\<open>subsubsection\<close> \<open>Some 3\<close>  \vspace{-0.1cm}
 
 Additional means assure that the following invariant is maintained in a document 
 conforming to \<^verbatim>\<open>scholarly_paper\<close>:
@@ -329,45 +379,47 @@ conforming to \<^verbatim>\<open>scholarly_paper\<close>:
 \center {\<open>level > 0\<close>}
 \<close>
 
-text\<open> The rest of the ontology introduces concepts for \<open>introductions\<close>, \<open>conclusion\<close>, \<open>related_work\<close>,
-\<open>bibliography\<close> etc. More details can be found in \<^verbatim>\<open>scholarly_paper\<close> contained ion the
-theory @{theory \<open>Isabelle_DOF.scholarly_paper\<close>}. \<close>
+text\<open> The rest of the ontology introduces concepts for \<^typ>\<open>introduction\<close>, \<^typ>\<open>conclusion\<close>,
+\<^typ>\<open>related_work\<close>, \<^typ>\<open>bibliography\<close> etc. More details can be found in \<^verbatim>\<open>scholarly_paper\<close>
+contained in the theory \<^theory>\<open>Isabelle_DOF.scholarly_paper\<close>. \<close>
 
-subsection\<open>Writing Academic Publications I : A Freeform Mathematics Text \<close>
+subsection\<open>Writing Academic Publications: A Freeform Mathematics Text \<close>
 text*[csp_paper_synthesis::technical, main_author = "Some bu"]\<open>We present a typical mathematical
-paper focussing on its form, not refering in any sense to its content which is out of scope here.
+paper focusing on its form, not referring in any sense to its content which is out of scope here.
 As mentioned before, we chose the paper~@{cite "taha.ea:philosophers:2020"} for this purpose,
 which is written in the so-called free-form style: Formulas are superficially parsed and 
-type-setted, but no deeper type-checking and checking with the underlying logical context
+type-set, but no deeper type-checking and checking with the underlying logical context
 is undertaken. \<close>
 
 figure*[fig0::figure,spawn_columns=False,relative_width="90",src="''figures/header_CSP_source.png''"]
        \<open> A mathematics paper as integrated document source ... \<close>  
 
 figure*[fig0B::figure,spawn_columns=False,relative_width="90",src="''figures/header_CSP_pdf.png''"]
-       \<open> \ldots and as corresponding \<^pdf>-output. \<close>  
+       \<open> ... and as corresponding \<^pdf>-output. \<close>  
 
-text\<open>The integrated source of this paper-except is shown in \<^figure>\<open>fig0\<close>, while the
+text\<open>The integrated source of this paper-excerpt is shown in \<^figure>\<open>fig0\<close>, while the
 document build process converts this to the corresponding \<^pdf>-output shown in \<^figure>\<open>fig0B\<close>.\<close>
 
 
 text\<open>Recall that the standard syntax for a text-element in \<^isadof> is 
 \<^theory_text>\<open>text*[<id>::<class_id>,<attrs>]\<open> ... text ...\<close>\<close>, but there are a few built-in abbreviations like
 \<^theory_text>\<open>title*[<id>,<attrs>]\<open> ... text ...\<close>\<close> that provide special command-level syntax for text-elements. 
-The other text-elements provide the authors and the abstract as specified by their class-id referring
-to the \<^theory_text>\<open>doc_class\<close>es of \<^verbatim>\<open>scholarly_paper\<close>; we say that these text elements are \<^emph>\<open>instances\<close> 
+The other text-elements provide the authors and the abstract as specified by their
+\<^emph>\<open>class\_id\<close>\<^index>\<open>class\_id@\<open>class_id\<close>\<close>
+referring to the \<^theory_text>\<open>doc_class\<close>es of \<^verbatim>\<open>scholarly_paper\<close>;
+we say that these text elements are \<^emph>\<open>instances\<close> 
 \<^bindex>\<open>instance\<close> of the \<^theory_text>\<open>doc_class\<close>es \<^bindex>\<open>doc\_class\<close> of the underlying ontology. \<close>
 
-text\<open>\vspace{1,5cm} The paper proceeds by providing instances for introduction, technical sections, 
+text\<open>The paper proceeds by providing instances for introduction, technical sections, 
 examples, \<^etc>. We would like to concentrate on one --- mathematical paper oriented --- detail in the 
 ontology \<^verbatim>\<open>scholarly_paper\<close>: 
 
 @{boxed_theory_text [display]
-\<open>doc_class technical = text_section +  . . .
+\<open>doc_class technical = text_section +  ...
 
 type_synonym tc = technical (* technical content *)
 
-datatype math_content_class = "defn"   | "axm"  | "thm"  | "lem" | "cor" | "prop" | ...
+datatype math_content_class = "defn" | "axm" | "thm"  | "lem" | "cor" | "prop" | ...
                            
 doc_class math_content = tc +   ...
 
@@ -379,53 +431,49 @@ doc_class "theorem"     = math_content +
 \<close>}\<close>
 
 
-text\<open>The class \<^verbatim>\<open>technical\<close> regroups a number of text-elements that contain typical 
-"technical content" in mathematical or engineering papers: code, definitions, theorems, 
-lemmas, examples. From this class, the more stricter class of @{typ \<open>math_content\<close>} is derived,
+text\<open>The class \<^typ>\<open>technical\<close> regroups a number of text-elements that contain typical 
+technical content in mathematical or engineering papers: code, definitions, theorems, 
+lemmas, examples. From this class, the stricter class of @{typ \<open>math_content\<close>} is derived,
 which is grouped into @{typ "definition"}s and @{typ "theorem"}s (the details of these
 class definitions are omitted here). Note, however, that class identifiers can be abbreviated by 
 standard \<^theory_text>\<open>type_synonym\<close>s for convenience and enumeration types can be defined by the 
 standard inductive \<^theory_text>\<open>datatype\<close> definition mechanism in Isabelle, since any HOL type is admitted
-for attibute declarations. Vice-versa, document class definitions imply a corresponding HOL type 
+for attribute declarations. Vice-versa, document class definitions imply a corresponding HOL type 
 definition. \<close>
 
 figure*[fig01::figure,spawn_columns=False,relative_width="95",src="''figures/definition-use-CSP.png''"]
        \<open> A screenshot of the integrated source with definitions ...\<close>  
-text\<open>An example for a sequence of (Isabelle-formula-) texts, their ontological declarations as 
-\<open>"definition"\<close>s in terms of the \<^verbatim>\<open>scholarly_paper\<close>-ontology and their type-conform referencing 
+text\<open>An example for a sequence of (Isabelle-formula-)texts, their ontological declarations as 
+\<^typ>\<open>definition\<close>s in terms of the \<^verbatim>\<open>scholarly_paper\<close>-ontology and their type-conform referencing 
 later is shown in \<^figure>\<open>fig01\<close> in its presentation as the integrated source.
 
 Note that the use in the ontology-generated antiquotation \<^theory_text>\<open>@{definition X4}\<close>
 is type-checked; referencing \<^verbatim>\<open>X4\<close> as \<^theory_text>\<open>theorem\<close> would be a type-error and be reported directly
 by \<^isadof> in Isabelle/jEdit. Note further, that if referenced correctly wrt. the sub-typing 
-hierarchy makes \<^verbatim>\<open>X4\<close> \<^emph>\<open>navigable\<close> in Isabelle/jedit; a click will cause the IDE to present the 
+hierarchy makes \<^verbatim>\<open>X4\<close> \<^emph>\<open>navigable\<close> in Isabelle/jEdit; a click will cause the IDE to present the 
 defining occurrence of this text-element in the integrated source.
 
-% TODO:
-% The definition \<^theory_text>\<open>@{definition X4}\<close> is not present in the screenshot,
-% it might be better to use  \<^theory_text>\<open>@{definition X22}\<close>.
-
 Note, further, how \<^isadof>-commands like \<^theory_text>\<open>text*\<close> interact with standard Isabelle document
 antiquotations described in the Isabelle Isar Reference Manual in Chapter 4.2 in great detail. 
-We refrain ourselves here to briefly describe three freeform antiquotations used her in this text:
+We refrain ourselves here to briefly describe three freeform antiquotations used in this text:
 
 \<^item>  the freeform term antiquotation, also called \<^emph>\<open>cartouche\<close>, written by
-   \<open>@{cartouche [style-parms] \<open>. . .\<close>\<close> or just by \<open>\<open>...\<close>\<close> if the list of style parameters
+   \<open>@{cartouche [style-parms] \<open>...\<close>}\<close> or just by \<open>\<open>...\<close>\<close> if the list of style parameters
    is empty,
-\<^item>  the freeform antiquotation for theory fragments written \<open>@{theory_text [style-parms] \<open>...\<close>\<close>
-   or just \<^verbatim>\<open>\<^theory_text> \<open>...\<close>\<close>  if the list of style parameters
-   is empty,  
+\<^item>  the freeform antiquotation for theory fragments written \<open>@{theory_text [style-parms] \<open>...\<close>}\<close>
+   or just \<^verbatim>\<open>\<^theory_text>\<close>\<open>\<open>...\<close>\<close> if the list of style parameters is empty,  
 \<^item>  the freeform antiquotations for verbatim, emphasized, bold, or footnote text elements.
 \<close>
 
 figure*[fig02::figure,spawn_columns=False,relative_width="95",src="''figures/definition-use-CSP-pdf.png''"]
-       \<open> ... and the corresponding pdf-oputput.\<close>  
+       \<open> ... and the corresponding \<^pdf>-output.\<close>  
 
 text\<open>
 \<^isadof> text-elements such as \<^theory_text>\<open>text*\<close> allow to have such standard term-antiquotations inside their
-text, permitting to give the whole text entity a formal, referentiable status with typed meta-
-information attached to it that may be used for presentation issues, search, or other technical
-purposes. The corresponding output of this snippet in the integrated source is shown in \<^figure>\<open>fig02\<close>. 
+text, permitting to give the whole text entity a formal, referentiable status with typed
+meta-information attached to it that may be used for presentation issues, search,
+or other technical purposes.
+The corresponding output of this snippet in the integrated source is shown in \<^figure>\<open>fig02\<close>. 
 \<close>
 
 
@@ -443,10 +491,10 @@ doc_class figure   = text_section +
 \<close>}
 \<close>
 figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figures/Dogfood-figures''"]
-       \<open> Declaring figures in the integrated source \ldots \<close>
+       \<open> Declaring figures in the integrated source.\<close>
 
 text\<open> 
-  The document class \<^boxed_theory_text>\<open>figure\<close> (supported by the \<^isadof> command abbreviation
+  The document class \<^typ>\<open>figure\<close> (supported by the \<^isadof> command abbreviation
   \<^boxed_theory_text>\<open>figure*\<close>) makes it possible to express the pictures and diagrams 
   as shown in \<^figure>\<open>fig_figures\<close>, which presents its own representation in the 
   integrated source as screenshot.\<close>
@@ -459,14 +507,11 @@ text\<open>
   doc_class article = 
      style_id :: string                <= "''LNCS''"
      version  :: "(int \<times> int \<times> int)"  <= "(0,0,0)"
-     where "(title       ~~ \<lbrakk>subtitle\<rbrakk>   ~~ \<lbrace>author\<rbrace>$^+$+  ~~  abstract    ~~
-               introduction ~~  \<lbrace>technical || example\<rbrace>$^+$  ~~  conclusion ~~  
-               bibliography)"
+     accepts "(title ~~ \<lbrakk>subtitle\<rbrakk> ~~ \<lbrace>author\<rbrace>\<^sup>+ ~~ abstract ~~ \<lbrace>introduction\<rbrace>\<^sup>+
+                   ~~ \<lbrace>background\<rbrace>\<^sup>* ~~ \<lbrace>technical || example \<rbrace>\<^sup>+ ~~ \<lbrace>conclusion\<rbrace>\<^sup>+
+                   ~~ bibliography ~~ \<lbrace>annex\<rbrace>\<^sup>* )"
   \<close>}\<close>
 
-  (*  % TODO:
-      % Update to the new implementation.
-      % where is deprecated and the new implementation uses accepts and rejects. *)
 text\<open>
   In a integrated document source, the body of the content can be paranthesized into:
 
@@ -478,7 +523,7 @@ text\<open>
 
 which signals to \<^isadof> begin and end of the part of the integrated source 
 in which the text-elements instances are expected to appear in the textual ordering 
-defined by \<^theory_text>\<open>article\<close>.
+defined by \<^typ>\<open>article\<close>.
 \<close>
 
 
@@ -491,12 +536,18 @@ side_by_side_figure*[exploring::side_by_side_figure,anchor="''fig-Dogfood-II-bgn
 
 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>Navigation via generated hyperlinks.\<close>
+                      src="''figures/Dogfood-IV-jumpInDocCLass''",
+                      anchor2="''fig:Dogfood-V-attribute''",
+                      caption2="''Exploring an attribute (hyperlinked to the class).''",
+                      relative_width2="47",
+                      src2="''figures/Dogfood-V-attribute''"]\<open>Navigation via generated hyperlinks.\<close>
+(* TODO: Update the images in fig:Dogfood-IV-jumpInDocCLass side_by_side_figure
+   to align them. This has to wait that the exploration of an attribute is again possible.
+   See: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/issues/10 *)
+
 text\<open> 
   From these class definitions, \<^isadof> also automatically generated editing 
-  support for Isabelle/jedit. In \autoref{fig-Dogfood-II-bgnd1} and 
+  support for Isabelle/jEdit. In \autoref{fig-Dogfood-II-bgnd1} and 
   \autoref{fig-bgnd-text_section} 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 
@@ -504,45 +555,53 @@ text\<open>
   \autoref{fig:Dogfood-V-attribute}) shows its type.
 \<close>
 
-figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-V-attribute''"]
-       \<open> Exploring an attribute (hyperlinked to the class). \<close> 
+figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-VI-linkappl.png''"]
+       \<open>Exploring an ontological reference.\<close> 
 
 text\<open> 
 An ontological reference application in @{figure "figDogfoodVIlinkappl"}: the 
-ontology-dependant antiquotation \<^boxed_theory_text>\<open>@ {example ...}\<close> 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,\<^ie>, Isabelle/jEdit
-will respond with an error.\<close>
+ontology-dependant antiquotation \<^boxed_theory_text>\<open>@{example \<open>ex1\<close>}\<close> refers to the corresponding 
+text-element \<^boxed_theory_text>\<open>ex1\<close>.
+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, \<^ie>,
+Isabelle/jEdit will respond with an error.\<close>
 
-section*[cenelec_onto::example]\<open>Writing Certification Documents (CENELEC\_50128)\<close>
+text\<open>We advise users to experiment with different notation variants.
+Note, further, that the Isabelle \<^latex>\<open>@\{cite ...\}\<close>-text-anti-quotation makes its checking
+on the level of generated \<^verbatim>\<open>.aux\<close>-files, which are not necessarily up-to-date. Ignoring the PIDE
+error-message and compiling a with a consistent bibtex usually makes disappear this behavior. 
+\<close>
+
+section*[cenelec_onto::example]\<open>Writing Certification Documents \<^boxed_theory_text>\<open>CENELEC_50128\<close>\<close>
 subsection\<open>The CENELEC 50128 Example\<close>
 text\<open> 
-  The ontology ``CENELEC\_50128''\index{ontology!CENELEC\_50128} is a small ontology modeling 
+  The ontology \<^verbatim>\<open>CENELEC_50128\<close>\index{ontology!CENELEC\_50128} is a small ontology modeling 
   documents for a certification following CENELEC 50128~@{cite "boulanger:cenelec-50128:2015"}.
   The \<^isadof> distribution contains a small example  using the ontology ``CENELEC\_50128'' in 
   the directory \nolinkurl{examples/CENELEC_50128/mini_odo/}. You can inspect/edit the 
   integrated source example by either 
-  \<^item> starting Isabelle/jedit using your graphical user interface (\<^eg>, by clicking on the 
+  \<^item> starting Isabelle/jEdit using your graphical user interface (\<^eg>, by clicking on the 
     Isabelle-Icon provided by the Isabelle installation) and loading the file 
     \nolinkurl{examples/CENELEC_50128/mini_odo/mini_odo.thy}.
-  \<^item> starting Isabelle/jedit from the command line by calling:
+  \<^item> starting Isabelle/jEdit from the command line by calling:
 
 @{boxed_bash [display]\<open>ë\prompt{\isadofdirn}ë 
   isabelle jedit examples/CENELEC_50128/mini_odo/mini_odo.thy \<close>}
 \<close>
 text\<open>\<^noindent> Finally, you
-  \<^item>   can build the PDF-document by calling:
-@{boxed_bash [display]\<open>ë\prompt{}ë isabelle build mini_odo \<close>}
+  \<^item>   can build the \<^pdf>-document by calling:
+@{boxed_bash [display]\<open>ë\prompt{\isadofdirn}ë isabelle build mini_odo \<close>}
 \<close>
  
 subsection\<open>Modeling CENELEC 50128\<close>
+
 text\<open>
   Documents to be provided in formal certifications (such as CENELEC 
   50128~@{cite "boulanger:cenelec-50128:2015"} or Common Criteria~@{cite "cc:cc-part3:2006"}) can 
   much profit from the control of ontological consistency:  a substantial amount of the work
   of evaluators in formal certification processes consists in  tracing down the links from 
   requirements over assumptions down to elements of evidence, be it in form of semi-formal 
-  documentation, models, code, or  tests.  In a certification process, traceability becomes a major 
+  documentation, models, code, or tests.  In a certification process, traceability becomes a major 
   concern; and providing mechanisms to ensure complete traceability already at the development of 
   the integrated source can in our view increase the speed and reduce the risk certification 
   processes. Making the link-structure machine-checkable, be it between requirements, assumptions, 
@@ -561,13 +620,6 @@ text\<open>
 @{boxed_theory_text [display]\<open>
 doc_class requirement = long_name :: "string option"
 
-doc_class requirement_analysis = no :: "nat"
-   where "requirement_item +"
-(*
-% TODO:
-% Update to the new implementation.
-% where is deprecated and the new implementation uses accepts and rejects. 
-*)
 doc_class hypothesis = requirement +
       hyp_type :: hyp_type <= physical  (* default *)
   
@@ -579,31 +631,31 @@ doc_class assumption = requirement +
 
 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 of 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 
+like an explication of what is precisely the difference between an \<^typ>\<open>hypothesis\<close> and an 
+\<^typ>\<open>assumption\<close> in the context of the evaluation standard. Since the PIDE makes for each 
 document class its definition available by a simple mouse-click, this kind on meta-knowledge 
 can be made far more accessible during the document evolution.
 
-For example, the term of category \<^emph>\<open>assumption\<close> is used for domain-specific assumptions. 
-It has formal, semi-formal and informal sub-categories. They have to be 
+For example, the term of category \<^typ>\<open>assumption\<close> is used for domain-specific assumptions. 
+It has \<^const>\<open>formal\<close>, \<^const>\<open>semiformal\<close> and \<^const>\<open>informal\<close> sub-categories. They have to be 
 tracked and discharged by appropriate validation procedures within a 
-certification process, be it by test or proof. It is different from a hypothesis, which is
+certification process, be it by test or proof. It is different from a \<^typ>\<open>hypothesis\<close>, which is
 globally assumed and accepted.
 
-In the sequel, the category \<^emph>\<open>exported constraint\<close> (or \<^emph>\<open>ec\<close> for short)
+In the sequel, the category \<^typ>\<open>exported_constraint\<close> (or \<^typ>\<open>EC\<close> for short)
 is used for formal assumptions, that arise during the analysis,
 design or implementation and have to be tracked till the final
 evaluation target, and discharged by appropriate validation procedures 
 within the certification process, be it by test or proof.  A particular class of interest 
-is the category \<^emph>\<open>safety related application condition\<close> (or \<^emph>\<open>SRAC\<close> 
-for short) which is used for \<^emph>\<open>ec\<close>'s that establish safety properties
+is the category \<^typ>\<open>safety_related_application_condition\<close> (or \<^typ>\<open>SRAC\<close> 
+for short) which is used for \<^typ>\<open>EC\<close>'s that establish safety properties
 of the evaluation target. Their traceability throughout the certification
 is therefore particularly critical. This is naturally modeled as follows:
 @{boxed_theory_text [display]\<open>  
-doc_class ec = assumption  +
+doc_class EC = assumption  +
      assumption_kind :: ass_kind <= (*default *) formal
                         
-doc_class SRAC = ec  +
+doc_class SRAC = EC  +
      assumption_kind :: ass_kind <= (*default *) formal
 \<close>}
 
@@ -617,45 +669,40 @@ text*[ass123::SRAC]\<open>
 \<close>
 \<close>}
 
-This will be shown in the PDF as follows:
+This will be shown in the \<^pdf> as follows:
 \<close>
-text*[ass123::SRAC] \<open> The overall sampling frequence of the odometer
+text*[ass123::SRAC] \<open> The overall sampling frequency of the odometer
 subsystem is therefore 14 khz, which includes sampling, computing and
 result communication times \ldots \<close>
 
-text\<open>Note that this pdf-output is the result of a specific setup for "SRAC"s.\<close>
+text\<open>Note that this \<^pdf>-output is the result of a specific setup for \<^typ>\<open>SRAC\<close>s.\<close>
 
 subsection*[ontopide::technical]\<open>Editing Support for CENELEC 50128\<close>  
 figure*[figfig3::figure,relative_width="95",src="''figures/antiquotations-PIDE''"]
 \<open> Standard antiquotations referring to theory elements.\<close>
 text\<open> The corresponding view in @{docitem  \<open>figfig3\<close>} shows core part of a document 
-conforming to the CENELEC 50128 ontology. The first sample shows standard Isabelle antiquotations 
+conforming to the \<^verbatim>\<open>CENELEC_50128\<close> ontology. The first sample shows standard Isabelle antiquotations 
 @{cite "wenzel:isabelle-isar:2020"} 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*[figfig5::figure, relative_width="95", src="''figures/srac-definition''"]
-        \<open> Defining a "SRAC" in the integrated source \ldots \<close>
-text\<open>
-TODO:
-The screenshot (figures/srac-definition) of the figure figfig5 should be updated
-to have a SRAC type in uppercase.
-\<close>
+        \<open> Defining a \<^typ>\<open>SRAC\<close> in the integrated source ... \<close>
 
 figure*[figfig7::figure, relative_width="95", src="''figures/srac-as-es-application''"]
-        \<open> Using a "SRAC" as "EC" document element. \<close>
-text\<open> The subsequent sample in @{figure \<open>figfig5\<close>} shows the definition of an
+        \<open> Using a \<^typ>\<open>SRAC\<close> as \<^typ>\<open>EC\<close> document element. \<close>
+text\<open> The subsequent sample in @{figure \<open>figfig5\<close>} shows the definition of a
 \<^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. 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. 
+are listed. \<^isadof>'s checks and establishes that this is legal in the given ontology. 
 \<close>    
 
 
 section*[tech_onto::example]\<open>Writing Technical Reports in \<^boxed_theory_text>\<open>technical_report\<close>\<close>  
 text\<open>While it is perfectly possible to write documents in the
-\<^boxed_theory_text>\<open>technical_report\<close> ontology in freeform-style (the present manual is mostly an
+\<^verbatim>\<open>technical_report\<close> ontology in freeform-style (the present manual is mostly an
 example for this category), we will briefly explain here the tight-checking-style in which
 most Isabelle reference manuals themselves are written. 
 
@@ -663,15 +710,15 @@ The idea has already been put forward by Isabelle itself; besides the general in
 which this work is also based, current Isabelle versions provide around 20 built-in 
 document and code antiquotations described in the Reference Manual pp.75 ff. in great detail.
 
-Most of them provide strict-checking, \<^ie> the argument strings where parsed and machine-checked in the
+Most of them provide strict-checking, \<^ie> the argument strings were parsed and machine-checked in the
 underlying logical context, which turns the arguments into \<^emph>\<open>formal content\<close> in the integrated
 source, in contrast to the free-form antiquotations which basically influence the presentation.
 
 We still mention a few of these document antiquotations here:
 \<^item> \<^theory_text>\<open>@{thm \<open>refl\<close>}\<close> or \<^theory_text>\<open>@{thm [display] \<open>refl\<close>}\<close> check that \<^theory_text>\<open>refl\<close> is indeed a reference
-  to a theorem; the additional "style" argument changes the presentation by printing the 
+  to a theorem; the additional ``style" argument changes the presentation by printing the 
   formula into the output instead of the reference itself,
-\<^item> \<^theory_text>\<open>@{lemma \<open>prop\<close> } by \<open>method\<close>\<close> allows to derive \<open>prop\<close> on the fly, thus garantee 
+\<^item> \<^theory_text>\<open>@{lemma \<open>prop\<close> } by \<open>method\<close>\<close> allows deriving \<open>prop\<close> on the fly, thus guarantee 
   that it is a corrollary of the current context,
 \<^item> \<^theory_text>\<open>@{term \<open>term\<close> }\<close> parses and type-checks \<open>term\<close>,
 \<^item> \<^theory_text>\<open>@{value \<open>term\<close> }\<close> performs the evaluation of \<open>term\<close>,
@@ -702,12 +749,13 @@ figure*[strict_SS::figure, relative_width="95", src="''figures/MyCommentedIsabel
 \<open>A table with a number of SML functions, together with their type.\<close>
 
 text\<open>
-\<open>TR_MyCommentedIsabelle\<close> is written according to the @{theory "Isabelle_DOF.technical_report"}
-ontology. \<^figure>\<open>strict_SS\<close> shows a snippet from this integrated source and gives an idea why 
+\<open>TR_MyCommentedIsabelle\<close> is written according to the \<^verbatim>\<open>technical_report\<close> ontology in
+\<^theory>\<open>Isabelle_DOF.technical_report\<close>.
+\<^figure>\<open>strict_SS\<close> shows a snippet from this integrated source and gives an idea why 
 its tight-checking allows for keeping track of underlying Isabelle changes:
 Any reference to an SML operation in some library module is type-checked, and the displayed
 SML-type really corresponds to the type of the operations in the underlying SML environment.
-In the pdf output, these text-fragments were displayed verbatim.
+In the \<^pdf> output, these text-fragments were displayed verbatim.
 \<close>
 
 
@@ -732,21 +780,21 @@ text\<open> This is *\<open>emphasized\<close> and this is a
 \<close>}
 
 Clearly, this is not always possible and, in fact, often \<^isadof> documents will contain 
-\<^LaTeX>-commands, this should be restricted to layout improvements that otherwise are (currently)
+\<^LaTeX>-commands, but this should be restricted to layout improvements that otherwise are (currently)
 not possible. As far as possible, the use of \<^LaTeX>-commands should be restricted to the definition 
 of ontologies and document templates (see @{docitem (unchecked) \<open>isadof_ontologies\<close>}).
 
 Restricting the use of \<^LaTeX> has two advantages: first, \<^LaTeX> commands can circumvent the 
 consistency checks of \<^isadof> and, hence, only if no \<^LaTeX> commands are used, \<^isadof> can 
-ensure that a document that does not generate any error messages in Isabelle/jedit also generated
-a PDF document. Second, future version of \<^isadof> might support different targets for the 
+ensure that a document that does not generate any error messages in Isabelle/jEdit also generated
+a \<^pdf> document. Second, future version of \<^isadof> might support different targets for the 
 document generation (\<^eg>, HTML) which, naturally, are only available to documents not using 
 too complex native \<^LaTeX>-commands. 
 
 Similarly, (unchecked) forward references should, if possible, be avoided, as they also might
 create dangling references during the document generation that break the document generation.  
 
-Finally, we recommend to use the @{command "check_doc_global"} command at the end of your 
+Finally, we recommend using the @{command "check_doc_global"} command at the end of your 
 document to check the global reference structure. 
 
 \<close>

examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy

@@ -1,7 +1,7 @@
 (*************************************************************************
  * Copyright (C) 
- *               2019-2021 University of Exeter 
- *               2018-2021 University of Paris-Saclay
+ *               2019-2022 University of Exeter 
+ *               2018-2022 University of Paris-Saclay
  *               2018      The University of Sheffield
  *
  * License:
@@ -22,12 +22,12 @@ chapter*[isadof_developers::text_section]\<open>Extending \<^isadof>\<close>
 text\<open>
   In this chapter, we describe the basic implementation aspects of \<^isadof>, which is based on 
   the following design-decisions:
-  \<^item> the entire \<^isadof> is a ``pure add-on,'' \<^ie>, we deliberately resign on the possibility to 
-    modify Isabelle itself.
+  \<^item> the entire \<^isadof> is a ``pure add-on,'' \<^ie>, we deliberately resign the possibility to 
+    modify Isabelle itself,
   \<^item> we made a small exception to this rule: the \<^isadof> package modifies in its installation 
-    about 10 lines in the \LaTeX-generator (\path{src/patches/thy_output.ML}).
+    about 10 lines in the \LaTeX-generator (\path{src/patches/thy_output.ML}),
   \<^item> we decided to make the markup-generation by itself to adapt it as well as possible to the 
-    needs of tracking the linking in documents.
+    needs of tracking the linking in documents,
   \<^item> \<^isadof> is deeply integrated into the Isabelle's IDE (PIDE) to give immediate feedback during 
     editing and other forms of document evolution.
 \<close>
@@ -57,8 +57,9 @@ text\<open>
    fun merge((d1,c1,...),(d2,c2,...)) = (merge_docobj_tab  (d1,d2,...), 
                                          merge_docclass_tab(c1,c2,...))
 );\<close>}
-  where the table  \<^boxed_sml>\<open>docobj_tab\<close> manages document classes and  \<^boxed_sml>\<open>docclass_tab\<close> the
-  environment for class definitions (inducing the inheritance relation). Other tables capture, \eg, 
+  where the table  \<^boxed_sml>\<open>docobj_tab\<close> manages document class instances
+  and \<^boxed_sml>\<open>docclass_tab\<close> the environment for class definitions
+  (inducing the inheritance relation). Other tables capture, \eg, 
   the class invariants, inner-syntax antiquotations. Operations follow the MVC-pattern, where 
   Isabelle/Isar provides the controller part. A typical model operation has the type:
 
@@ -75,7 +76,7 @@ in  (Data.map(apfst decl)(ctxt)
   handle Symtab.DUP _ =>
               error("multiple declaration of document reference"))
 end\<close>}
-  where \<^boxed_theory_text>\<open>Data.map\<close> is the update function resulting from the instantiation of the 
+  where \<^boxed_sml>\<open>Data.map\<close> is the update function resulting from the instantiation of the 
   functor  \<^boxed_sml>\<open>Generic_Data\<close>. This code fragment uses operations from a library structure 
    \<^boxed_sml>\<open>Symtab\<close> that were used to update the appropriate table for document objects in
   the plugin-local state. Possible exceptions to the update operation were mapped to a system-global 
@@ -91,7 +92,7 @@ op >>     : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
 op option : ('a -> 'b * 'a) -> 'a -> 'b option * 'a
 op repeat : ('a -> 'b * 'a) -> 'a -> 'b list * 'a \<close>}
   for alternative, sequence, and piping, as well as combinators for option and repeat. Parsing 
-  combinators have the advantage that they can be smoothlessly integrated into standard programs, 
+  combinators have the advantage that they can be integrated into standard programs, 
   and they enable the dynamic extension of the grammar. There is a more high-level structure 
   \inlinesml{Parse} providing specific combinators for the command-language Isar:
 
@@ -106,7 +107,7 @@ val attributes =(Parse.$$$ "[" |-- (reference
                    |--(Parse.enum ","attribute)))[]))--| Parse.$$$ "]"              
 \end{sml}                                            
 
-  The ``model'' \<^boxed_theory_text>\<open>declare_reference_opn\<close> and ``new'' \<^boxed_theory_text>\<open>attributes\<close> parts were 
+  The ``model'' \<^boxed_sml>\<open>declare_reference_opn\<close> and ``new'' \<^boxed_sml>\<open>attributes\<close> parts were 
   combined via the piping operator and registered in the Isar toplevel:
 
 @{boxed_sml [display]
@@ -141,30 +142,31 @@ text\<open>
                                    (docitem_antiq_gen default_cid) #>
           ML_Antiquotation.inline  <@>{binding docitem_value} 
                                    ML_antiq_docitem_value)\<close>}
-  the text antiquotation \<^boxed_theory_text>\<open>docitem\<close> is declared and bounded to a parser for the argument 
+  the text antiquotation \<^boxed_sml>\<open>docitem\<close> is declared and bounded to a parser for the argument 
   syntax and the overall semantics. This code defines a generic antiquotation to be used in text 
   elements such as
 
 @{boxed_theory_text [display]\<open>
-text\<open>as defined in <@>{docitem \<open>d1\<close>} ...\<close>
+text\<open>as defined in @{docitem \<open>d1\<close>} ...\<close>
 \<close>}
 
-  The subsequent registration \<^boxed_theory_text>\<open>docitem_value\<close> binds code to a ML-antiquotation usable 
+  The subsequent registration \<^boxed_sml>\<open>docitem_value\<close> binds code to a ML-antiquotation usable 
   in an ML context for user-defined extensions; it permits the access to the current ``value'' 
-  of document element, \ie; a term with the entire update history.
+  of document element, \<^ie>, a term with the entire update history.
 
   It is possible to generate antiquotations \emph{dynamically}, as a consequence of a class 
-  definition in ODL. The processing of the ODL class \<^boxed_theory_text>\<open>definition\<close> also \emph{generates}
-  a text antiquotation \<^boxed_theory_text>\<open>@{definition \<open>d1\<close>}\<close>, which works similar to 
+  definition in ODL. The processing of the ODL class \<^typ>\<open>definition\<close> also \emph{generates}
+  a text antiquotation \<^boxed_theory_text>\<open>@{"definition" \<open>d1\<close>}\<close>, which works similar to 
   \<^boxed_theory_text>\<open>@{docitem \<open>d1\<close>}\<close> except for an additional type-check that assures that 
   \<^boxed_theory_text>\<open>d1\<close> is a reference to a definition. These type-checks support the subclass hierarchy.
 \<close>
 
 section\<open>Implementing Second-level Type-Checking\<close>
+
 text\<open>
   On expressions for attribute values, for which we chose to use HOL syntax to avoid that users 
   need to learn another syntax, we implemented an own pass over type-checked terms. Stored in the 
-  late-binding table \<^boxed_theory_text>\<open>ISA_transformer_tab\<close>, we register for each inner-syntax-annotation 
+  late-binding table \<^boxed_sml>\<open>ISA_transformer_tab\<close>, we register for each inner-syntax-annotation 
   (ISA's), a function of type
 
 @{boxed_sml [display]
@@ -180,52 +182,35 @@ text\<open>
 
 section\<open>Programming Class Invariants\<close>
 text\<open>
-  For the moment, there is no high-level syntax for the definition of class invariants. A 
-  formulation, in SML, of the first class-invariant in @{docitem "sec:class_inv"} is straight-forward:
-
-@{boxed_sml [display]
-\<open>fun check_result_inv oid {is_monitor:bool} ctxt =
-  let val kind = compute_attr_access ctxt "kind" oid <@>{here} <@>{here} 
-      val prop = compute_attr_access ctxt "property" oid <@>{here} <@>{here} 
-      val tS = HOLogic.dest_list prop
-  in  case kind_term of
-       <@>{term "proof"} => if not(null tS) then true
-                          else error("class result invariant violation") 
-      | _ => false
-  end
- val _ = Theory.setup (DOF_core.update_class_invariant 
-                                "tiny_cert.result" check_result_inv)\<close>}
-
-  The \<^boxed_sml>\<open>setup\<close>-command (last line) registers the \<^boxed_theory_text>\<open>check_result_inv\<close> function 
-  into the \<^isadof> kernel, which activates any creation or modification of an instance of
-  \<^boxed_theory_text>\<open>result\<close>.  We cannot replace \<^boxed_theory_text>\<open>compute_attr_access\<close> by the corresponding 
-  antiquotation \<^boxed_theory_text>\<open>@{docitem_value kind::oid}\<close>, since \<^boxed_theory_text>\<open>oid\<close> is
-  bound to a variable here and can therefore not be statically expanded.
+  See \<^technical>\<open>sec:low_level_inv\<close>.
 \<close>
 
 section\<open>Implementing Monitors\<close>
+
 text\<open>
   Since monitor-clauses have a regular expression syntax, it is natural to implement them as 
-  deterministic automata. These are stored in the  \<^boxed_theory_text>\<open>docobj_tab\<close> for monitor-objects 
+  deterministic automata. These are stored in the  \<^boxed_sml>\<open>docobj_tab\<close> for monitor-objects 
   in the \<^isadof> component. We implemented the functions:
 
 @{boxed_sml [display]
 \<open>  val  enabled : automaton -> env -> cid list
    val  next    : automaton -> env -> cid -> automaton\<close>}
-  where \<^boxed_theory_text>\<open>env\<close> is basically a map between internal automaton states and class-id's 
-  (\<^boxed_theory_text>\<open>cid\<close>'s). An automaton is said to be \<^emph>\<open>enabled\<close> for a class-id, 
+  where \<^boxed_sml>\<open>env\<close> is basically a map between internal automaton states and class-id's 
+  (\<^boxed_sml>\<open>cid\<close>'s). An automaton is said to be \<^emph>\<open>enabled\<close> for a class-id, 
   iff it either occurs in its accept-set or its reject-set (see @{docitem "sec:monitors"}). During 
   top-down document validation, whenever a text-element is encountered, it is checked if a monitor 
-  is \emph{enabled} for this class; in this case, the \<^boxed_theory_text>\<open>next\<close>-operation is executed. The 
-  transformed automaton recognizing the rest-language is stored in \<^boxed_theory_text>\<open>docobj_tab\<close> if
-  possible; otherwise, if \<^boxed_theory_text>\<open>next\<close> fails, an error is reported. The automata implementation 
+  is \emph{enabled} for this class; in this case, the \<^boxed_sml>\<open>next\<close>-operation is executed. The 
+  transformed automaton recognizing the rest-language is stored in \<^boxed_sml>\<open>docobj_tab\<close> if
+  possible;
+  % TODO: clarify the notion of rest-language
+  otherwise, if \<^boxed_sml>\<open>next\<close> fails, an error is reported. The automata implementation
   is, in large parts, generated from a formalization of functional automata~\cite{nipkow.ea:functional-Automata-afp:2004}.
 \<close>
 
-section\<open>The \LaTeX-Core of \<^isadof>\<close>
+section\<open>The \<^LaTeX>-Core of \<^isadof>\<close>
 text\<open>
-  The \LaTeX-implementation of \<^isadof> heavily relies on the 
-  ``keycommand''~@{cite "chervet:keycommand:2010"} package. In fact, the core \<^isadof> \LaTeX-commands
+  The \<^LaTeX>-implementation of \<^isadof> heavily relies on the 
+  ``keycommand''~@{cite "chervet:keycommand:2010"} package. In fact, the core \<^isadof> \<^LaTeX>-commands
   are just wrappers for the corresponding commands from the keycommand package:
 
 @{boxed_latex [display]
@@ -236,9 +221,9 @@ text\<open>
 \newcommand\provideisadof[1]{%
   \expandafter\providekeycommand\csname isaDof.#1\endcsname}%\<close>}
 
-  The \LaTeX-generator of \<^isadof> maps each \<^boxed_theory_text>\<open>doc_item\<close> to an \LaTeX-environment (recall
-  @{docitem "text-elements"}). As generic \<^boxed_theory_text>\<open>doc_item\<close> are derived from the text element, 
-  the enviornment \inlineltx|{isamarkuptext*}| builds the core of \<^isadof>'s \LaTeX{} implementation. 
+  The \<^LaTeX>-generator of \<^isadof> maps each \<^boxed_theory_text>\<open>doc_item\<close> to an \<^LaTeX>-environment (recall
+  @{docitem "text-elements"}). As generic \<^boxed_theory_text>\<open>doc_item\<close>s are derived from the text element, 
+  the environment \inlineltx|isamarkuptext*| builds the core of \<^isadof>'s \<^LaTeX> implementation. 
   For example, the @{docitem "ass123"} from page \pageref{ass123} is mapped to
 
 @{boxed_latex [display]
@@ -251,7 +236,7 @@ text\<open>
  times ...
 \end{isamarkuptext*}\<close>}
 
-This environment is mapped to a plain \LaTeX command via (again, recall @{docitem "text-elements"}):
+This environment is mapped to a plain \<^LaTeX> command via (again, recall @{docitem "text-elements"}):
 @{boxed_latex [display]
 \<open> \NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}} \<close>}
 

examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy

@@ -19,6 +19,8 @@ close_monitor*[this]
 check_doc_global
 text\<open>Resulting trace in \<^verbatim>\<open>doc_item\<close> ''this'': \<close>
 ML\<open>@{trace_attribute this}\<close>
+
+ 
 end
 (*>*) 
 

examples/technical_report/Isabelle_DOF-Manual/ROOT

@@ -21,6 +21,7 @@ session "Isabelle_DOF-Manual" = "Isabelle_DOF" +
     "figures/Dogfood-Intro.png"
     "figures/Dogfood-IV-jumpInDocCLass.png"
     "figures/Dogfood-V-attribute.png"
+    "figures/Dogfood-VI-linkappl.png"
     "figures/isabelle-architecture.pdf"
     "figures/isabelle-architecture.svg"
     "figures/isadof.png"

examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex

@@ -21,7 +21,7 @@
 \usepackage{xcolor}
 \usepackage{lstisadof-manual}
 \usepackage{xspace}
-\usepackage{dtk-logos}
+\IfFileExists{hvlogos.sty}{\usepackage{hvlogos}}{\newcommand{\TeXLive}{\TeX Live}\newcommand{\BibTeX}{Bib\TeX}}
 \usepackage{railsetup}
 \setcounter{secnumdepth}{2}
 \usepackage{index}
@@ -41,8 +41,8 @@
 \pagestyle{headings}
 
 \uppertitleback{
-Copyright \copyright{} 2019--2021 University of Exeter, UK\\
-\phantom{Copyright \copyright{}} 2018--2021 Universit\'e Paris-Saclay, France\\
+Copyright \copyright{} 2019--2022 University of Exeter, UK\\
+\phantom{Copyright \copyright{}} 2018--2022 Universit\'e Paris-Saclay, France\\
 \phantom{Copyright \copyright{}} 2018--2019 The University of Sheffield, UK\\
 
 \smallskip
@@ -77,11 +77,13 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 
 \lowertitleback{%
 This manual describes \isadof version \isadofversion.  The latest official 
-release is \isadoflatestversion{} (\href{https://doi.org/\isadoflatestdoi}{doi:\isadoflatestdoi}). The DOI \href{https://doi.org/\isadofgenericdoi}{\isadofgenericdoi} will allways point to the latest release.  The latest development version as well as official releases are available at 
+release is \isadoflatestversion{} (\href{https://doi.org/\isadoflatestdoi}{doi:\isadoflatestdoi}). 
+The DOI \href{https://doi.org/\isadofgenericdoi}{\isadofgenericdoi} will allways point to the latest 
+release.  The latest development version as well as official releases are available at 
 \url{\dofurl}.
 
 \paragraph*{Contributors.} We would like to thank the following contributors to \isadof 
-(in alphabetical order): Idir Ait-Sadoune, Paolo Crisafulli, Chantal Keller, and Nicolas M{\'e}ric.
+(in alphabetical order): Idir Ait-Sadoune, Paolo Crisafulli, and Nicolas M{\'e}ric.
 
 \paragraph*{Acknowledgments.} This work has been partially supported by IRT SystemX, Paris-Saclay, 
 France, and therefore granted with public funds of the Program ``Investissements d'Avenir.''
@@ -107,7 +109,7 @@ France, and therefore granted with public funds of the Program ``Investissements
   \hfill
   \begin{minipage}{8cm}
     \raggedleft\normalsize
-    Laboratoire en Recherche en Informatique (LRI)\\
+    Laboratoire des Methodes Formelles (LMF)\\
     Universit\'e Paris-Saclay\\
     91405 Orsay Cedex\\
     France

examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy

@@ -22,7 +22,7 @@ define_shortcut* isabelle \<rightleftharpoons> \<open>Isabelle/HOL\<close>
 open_monitor*[this::report] 
 (*>*)
 
-title*[tit::title]\<open>My Personal, Ecclectic Isabelle Programming Manual\<close> 
+title*[tit::title]\<open>My Personal, Eclectic Isabelle Programming Manual\<close> 
 subtitle*[stit::subtitle]\<open>Version : Isabelle 2020\<close>
 text*[bu::author,     
       email       = "''wolff@lri.fr''",
@@ -46,7 +46,7 @@ text*[abs::abstract,
   This text is written itself in Isabelle/Isar using a specific document ontology
   for technical reports. It is intended to be a "living document", i.e. it is not only
   used for generating a static, conventional .pdf, but also for direct interactive 
-  exploration in Isabelle/jedit. This way, types, intermediate results of computations and
+  exploration in Isabelle/jEdit. This way, types, intermediate results of computations and
   checks can be repeated by the reader who is invited to interact with this document.
   Moreover, the textual parts have been enriched with a maximum of formal content
   which makes this text re-checkable at each load and easier maintainable.
@@ -71,7 +71,7 @@ text\<open> \<^vs>\<open>-0.5cm\<close>
   in Isabelle/jedit in order to make experiments on the running code. This text is written 
   itself in Isabelle/Isar using a specific document ontology for technical reports. It is 
   intended to be a "living document", i.e. it is not only used for generating a static, 
-  conventional .pdf, but also for direct interactive exploration in Isabelle/jedit. This way, 
+  conventional .pdf, but also for direct interactive exploration in Isabelle/jEdit. This way, 
   types, intermediate results of computations and checks can be repeated by the reader who is 
   invited to interact with this document. Moreover, the textual parts have been enriched with a 
   maximum of formal content which makes this text re-checkable at each load and easier 
@@ -81,7 +81,7 @@ figure*[architecture::figure,relative_width="70",src="''figures/isabelle-archite
      The system architecture of Isabelle (left-hand side) and the  asynchronous communication 
      between the Isabelle system and the IDE (right-hand side). \<close>
 
-text\<open>This programming roughly follows the Isabelle system architecture shown in 
+text\<open>This programming tutorial roughly follows the Isabelle system architecture shown in 
   \<^figure>\<open>architecture\<close>, and, to be more precise, more or less in the bottom-up order.
 
   We start from the basic underlying SML platform over the Kernels to the tactical layer 
@@ -92,8 +92,8 @@ chapter*[t1::technical]\<open> SML and Fundamental SML libraries  \<close>
 
 section*[t11::technical] "ML, Text and Antiquotations"
 
-text\<open>Isabelle is written in SML, the "Standard Meta-Language", which is is an impure functional 
-  programming language allowing, in principle, mutable variables and side-effects. 
+text\<open>Isabelle is written in SML, the "Standard Meta-Language", which is an impure functional 
+  programming language allowing, in principle, mutable variables and side effects. 
   The following Isabelle/Isar commands allow for accessing the underlying SML interpreter
   of Isabelle directly. In the example, a mutable variable X is declared, initialized to 0 and 
   updated; and finally re-evaluated leading to output: \<close>
@@ -142,14 +142,14 @@ text\<open>\<^emph>\<open>This is a text.\<close>\<close>
 
 text\<open>... is represented in the integrated source (the \<^verbatim>\<open>.thy\<close> file) by:\<close>
 
-text\<open> *\<open>\<open>\<close>This is a text.\<open>\<close>\<close>\<close>
+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>
+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''"]
-        \<open>A text-element as presented in Isabelle/jedit.\<close>
+        \<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 
+text\<open>The text-commands, ML-commands (and in principle any other command) can be seen as 
   \<^emph>\<open>quotations\<close> over the underlying SML environment (similar to OCaml or Haskell).
   Linking these different sorts of quotations with each other and the underlying SML-environment
   is supported via \<^emph>\<open>antiquotations\<close>'s. Generally speaking, antiquotations are a kind of semantic
@@ -192,7 +192,7 @@ text\<open>\<^vs>\<open>-1.0cm\<close>... which we will describe in more detail
 
 text\<open>In a way, anti-quotations implement a kind of 
   literate specification style in text, models, code, proofs, etc., which become alltogether
-  elements of one global \<^emph>\<open>integrated document\<close> in which mutual dependencies can be machine=checked
+  elements of one global \<^emph>\<open>integrated document\<close> in which mutual dependencies can be machine-checked
   (i.e. \<open>formal\<close> in this sense).
   Attempting to maximize the \<open>formal content\<close> is a way to ensure "Agile Development" (AD) of an 
   integrated document development, in the sense that it allows to give immediate feedback
@@ -210,17 +210,21 @@ text\<open>It is instructive to study the fundamental bootstrapping sequence of
   it is written in the Isar format and gives an idea of the global module dependencies: 
   \<^file>\<open>~~/src/Pure/ROOT.ML\<close>. Loading this file 
   (for example by hovering over this hyperlink in the antiquotation holding control or
-  command key in Isabelle/jedit and activating it) allows the Isabelle IDE 
+  command key in Isabelle/jEdit and activating it) allows the Isabelle IDE 
   to support hyperlinking \<^emph>\<open>inside\<close> the Isabelle source.\<close>
 
 text\<open>The bootstrapping sequence is also reflected in the following diagram @{figure "architecture"}.\<close>
 
 
-section*[t12::technical] "Elements of the SML library";  
+section*[t12::technical] "Elements of the SML library"  
 text\<open>Elements of the \<^file>\<open>~~/src/Pure/General/basics.ML\<close>  SML library
   are basic exceptions. Note that exceptions should be catched individually, uncatched exceptions 
   except those generated by the specific "error" function are discouraged in Isabelle
-  source programming since they might produce races in the internal Isabelle evaluation. 
+  source programming since they might produce races in the internal Isabelle evaluation.
+  % TODO:
+  % The following exceptions are defined in $ML_SOURCES/basis/General.sml
+  % and in $ISABELLE_HOME/src/Pure/general/scan.ml
+  % ans not in \<^file>\<open>~~/src/Pure/General/basics.ML\<close>
   
 \<^item> \<^ML>\<open>Bind      : exn\<close> \<^vs>\<open>-0.3cm\<close>
 \<^item> \<^ML>\<open>Chr       : exn\<close>  \<^vs>\<open>-0.3cm\<close>
@@ -251,7 +255,11 @@ text*[squiggols::technical]
 \<^item> @{ML "op --| : ('a->'b*'c) * ('c->'d*'e)->'a->'b*'e"}, parse pair, forget left \<^vs>\<open>-0.3cm\<close>
 \<^item> @{ML "op ?  : bool * ('a->'a)->'a->'a"}, if then else  \<^vs>\<open>-0.3cm\<close>
 \<^item> @{ML "ignore   : 'a->unit"}, force execution, but ignore result \<^vs>\<open>-0.3cm\<close>
-\<^item> @{ML "op before: ('a*unit) -> 'a"} \<^vs>\<open>-0.8cm\<close> \<close>
+\<^item> @{ML "op before: ('a*unit) -> 'a"} \<^vs>\<open>-0.8cm\<close>
+% TODO:
+% Again the definitions of these operators span multiple files
+% and not just \<^file>\<open>~~/src/Pure/General/basics.ML\<close>.
+\<close>
 
 text\<open>\<^noindent> Some basic examples for the programming style using these combinators can be found in the
 "The Isabelle Cookbook" section 2.3.\<close>
@@ -300,7 +308,9 @@ text\<open> What I call the 'Nano-Kernel' in Isabelle can also be seen as an acy
   "Generic theory contexts with unique identity, arbitrarily typed data,
   monotonic development graph and history support.  Generic proof
   contexts with arbitrarily typed data."
-  
+  % NOTE:
+  % Add the reference.
+
   In my words: a context is essentially a container with
   \<^item> an id
   \<^item> a list of parents (so: the graph structure)
@@ -339,8 +349,6 @@ text\<open>
 \<^item> \<^ML>\<open>Context.map_theory: (theory -> theory) -> Context.generic -> Context.generic\<close>
 \<close>
 
-text\<open>\<^ML>\<open>3+4\<close>\<close>
-
 text\<open>The structure \<^ML_structure>\<open>Proof_Context\<close> provides a key data-structures concerning contexts:
 
 \<^item> \<^ML>\<open> Proof_Context.init_global: theory -> Proof.context\<close>
@@ -359,7 +367,7 @@ text\<open>A central mechanism for constructing user-defined data is by the \<^M
   \<^verbatim>\<open>empty\<close>, and operations  \<^verbatim>\<open>merge\<close> and \<^verbatim>\<open>extend\<close>, can construct a lense with operations
   \<^verbatim>\<open>get\<close> and \<^verbatim>\<open>put\<close> that attach this data into the generic system context. Rather than using
   unsynchronized SML mutable variables, this is the mechanism to introduce component local
-  data in Isabelle, which allows to manage this data for the necessary backtrack- and synchronization
+  data in Isabelle, which allows to manage this data for the necessary backtrack and synchronization
   features in the pervasively parallel evaluation framework that Isabelle as a system represents.\<close>
 
 ML \<open>
@@ -476,17 +484,21 @@ ML\<open> val Const ("HOL.implies", @{typ "bool \<Rightarrow> bool \<Rightarrow>
 
  val "HOL.bool" = @{type_name "bool"};
 
- (* three ways to write type bool:@ *)
+ (* three ways to write type bool: *)
  val Type("fun",[s,Type("fun",[@{typ "bool"},Type(@{type_name "bool"},[])])]) = @{typ "bool \<Rightarrow> bool \<Rightarrow> bool"};
  
 \<close>
+text\<open>
+% NOTE:
+% The quotes disappear in the pdf document output.
 
+\<close>
 text\<open>Note that the SML interpreter is configured that he will actually print a type
      \<^verbatim>\<open>Type("HOL.bool",[])\<close> just as \<^verbatim>\<open>"bool": typ\<close>, so a compact notation looking
      pretty much like a string. This can be confusing at times.\<close>
 
 text\<open>Note, furthermore, that there is a programming API for the HOL-instance of Isabelle:
-  it is contained in @{file  "$ISABELLE_HOME/src/HOL/Tools/hologic.ML"}. It offers for many
+  it is contained in @{file  "$ISABELLE_HOME/src/HOL/Tools/hologic.ML"}. It offers many
   operators of the HOL logic specific constructors and destructors:\<close>
 
 text*[T2::technical]\<open>
@@ -963,9 +975,9 @@ text\<open>At this point, we leave the Pure-Kernel and start to describe the fir
 
 text\<open> \<^ML_type>\<open>tactic\<close>'s are in principle \<^emph>\<open>relations\<close> on theorems  \<^ML_type>\<open>thm\<close>; the relation is
   lazy and encoded as function of type \<^ML_type>\<open>thm -> thm Seq.seq\<close>.
-  This gives a
-  natural way to represent the fact that HO-Unification (and therefore the mechanism of rule-instan-
-  tiation) are non-deterministic in principle. Heuristics may choose particular preferences between 
+  This gives a natural way to represent the fact that HO-Unification
+  (and therefore the mechanism of rule-instantiation) are non-deterministic in principle.
+  Heuristics may choose particular preferences between 
   the theorems in the range of this relation, but the Isabelle Design accepts this fundamental 
   fact reflected at this point in the prover architecture. 
   This potentially infinite relation is implemented by a function of theorems to lazy lists 
@@ -994,9 +1006,9 @@ text\<open>The next layer in the architecture describes  \<^ML_type>\<open>tacti
   theorems  in a backward reasoning style (bottom up development of proof-trees). An initial 
   goal-state for some property \<^prop>\<open>A\<close> --- the \<^emph>\<open>goal\<close> --- is constructed via the kernel 
   \<^ML>\<open>Thm.trivial\<close>-operation into  \<^prop>\<open>A \<Longrightarrow> A\<close>, and tactics either refine the premises --- the 
-  \<^emph>\<open>subgoals\<close> the of this meta-implication --- producing  more and more of them or eliminate them 
+  \<^emph>\<open>subgoals\<close> of this meta-implication --- producing  more and more of them or eliminate them 
   in subsequent goal-states. Subgoals of the form \<^prop>\<open>B\<^sub>1 \<Longrightarrow> B\<^sub>2 \<Longrightarrow> A \<Longrightarrow> B\<^sub>3 \<Longrightarrow> B\<^sub>4 \<Longrightarrow> A\<close> can be 
-  eliminated via the  \<^ML>\<open>Tactic.assume_tac\<close>-tactic, and a subgoal  \<^prop>\<open>C\<^sub>m\<close> can be refined via the 
+  eliminated via the \<^ML>\<open>Tactic.assume_tac\<close>-tactic, and a subgoal  \<^prop>\<open>C\<^sub>m\<close> can be refined via the 
   theorem \<^prop>\<open>E\<^sub>1 \<Longrightarrow> E\<^sub>2 \<Longrightarrow> E\<^sub>3 \<Longrightarrow> C\<^sub>m\<close> the \<^ML>\<open>Tactic.resolve_tac\<close> - tactic to new subgoals
   \<^prop>\<open>E\<^sub>1\<close>, \<^prop>\<open>E\<^sub>2\<close>, \<^prop>\<open>E\<^sub>3\<close>. In case that a theorem used for resolution has no premise \<^prop>\<open>E\<^sub>i\<close>, 
   the subgoal  \<^prop>\<open>C\<^sub>m\<close> is also eliminated ("closed").
@@ -1037,7 +1049,7 @@ text\<open>Note that "applying a rule" is a fairly complex operation in the Exte
   \<^prop>\<open>D\<^sub>2\<close> and \<^prop>\<open>A\<close> have been replaced by schematic variables (see phase one),
   they must be replaced by parameterized schematic variables, i. e. a kind of skolem function.
   For example, \<open>?x + ?y = ?y + ?x\<close> would be lifted to 
-  \<open>!!  x y z. ?x x y z + ?y x y z = ?y x y z + ?x x y z\<close>. This way, the lifted theorem
+  \<open>\<And>  x y z. ?x x y z + ?y x y z = ?y x y z + ?x x y z\<close>. This way, the lifted theorem
   can be instantiated by the parameters  \<open>x y z\<close> representing "fresh free variables"
   used for this sub-proof. This mechanism implements their logically correct bookkeeping via
   kernel primitives.
@@ -1122,13 +1134,13 @@ thm "thm111"
 section\<open>Toplevel --- aka. ''The Isar Engine''\<close>
 
 text\<open>  The main structure of the Isar-engine is \<^ML_structure>\<open>Toplevel\<close>.
-   The Isar Toplevel (aka "the Isar engine" or the "Isar Interpreter") is an transaction
+   The Isar Toplevel (aka "the Isar engine" or the "Isar Interpreter") is a transaction
    machine sitting over the Isabelle Kernel steering some asynchronous evaluation during the
    evaluation of Isabelle/Isar input, usually stemming from processing Isabelle \<^verbatim>\<open>.thy\<close>-files. \<close>
 
 subsection*[tplstate::technical] \<open>Toplevel Transaction Management in the Isar-Engine\<close>
 text\<open>
-   The  structure \<^ML_structure>\<open>Toplevel\<close>  provides and internal \<^ML_type>\<open>state\<close> with the 
+   The  structure \<^ML_structure>\<open>Toplevel\<close>  provides an internal \<^ML_type>\<open>state\<close> with the 
    necessary infrastructure ---  i.e. the operations to pack and unpack theories and
    queries  on it:
 
@@ -1186,7 +1198,7 @@ text\<open>
  with a few query operations on the state of the toplevel:
  \<^item>  \<^ML>\<open>Outer_Syntax.command : Outer_Syntax.command_keyword -> string -> 
                               (Toplevel.transition -> Toplevel.transition) parser -> unit\<close>,
- \<^item>  \<^ML>\<open>Document.state : unit -> Document.state\<close>, giving the state as a "collection of named
+ \<^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,
@@ -1214,7 +1226,7 @@ text\<open> The integration of the  \<^theory_text>\<open>text\<close>-command i
  \<close>}
 
  where \<^ML>\<open>Pure_Syn.document_command\<close> is the defining operation for the 
- "diagnostic" (=side-effect-free) toplevel operation \<^ML>\<open>Pure_Syn.document_command\<close> looks as follows:
+ "diagnostic" (=side-effect-free) toplevel operation. \<^ML>\<open>Pure_Syn.document_command\<close> looks as follows:
 
  @{ML [display]\<open> let fun output_document state markdown txt = 
                            Thy_Output.output_document (Toplevel.presentation_context state) markdown txt
@@ -1272,7 +1284,7 @@ text\<open>The toplevel also provides an infrastructure for managing configurati
 \<close>
 
 
-subsubsection*[ex::example]\<open>Example registration of an config attribute \<close>
+subsubsection*[ex::example]\<open>Example registration of a config attribute \<close>
 text\<open>The attribute XS232 is initialized by false:\<close>
 ML\<open> 
 val (XS232, XS232_setup)
@@ -1436,31 +1448,31 @@ text\<open>A \<^verbatim>\<open>.thy\<close> file consists of a \<^emph>\<open>h
   predefined commands allow for the dynamic creation of new commands similarly 
   to the definition of new functions in an interpreter shell (or: toplevel, see above.).
   A command starts with a pre-declared keyword and specific syntax of this command;
-  the declaration of a keyword is only allowed in the same \<^verbatim>\<open>.thy\<close>-file where the
+  the declaration of a keyword is only allowed in the same \<^verbatim>\<open>.thy\<close>-file where
   the corresponding new command is defined. The semantics of the command is expressed
   in ML and consists of a @{ML_type "Toplevel.transition -> Toplevel.transition"}
   function. Thus, the Isar-toplevel supports the generic document model 
   and allows for user-programmed extensions.\<close>
 
-text\<open>In the traditional literature, Isabelle \<^verbatim>\<open>.thy\<close>-files were 
-  were said to be processed by processed by two types of parsers:
+text\<open>In the traditional literature, Isabelle \<^verbatim>\<open>.thy\<close>-files 
+  were said to be processed by two types of parsers:
 \<^enum> the "outer-syntax" (i.e. the syntax for commands) is processed 
   by a lexer-library and parser combinators built on top, and
-\<^enum> the "inner-syntax" (i.e. the syntax for @{term \<open>\<Lambda>\<close>} - terms) 
+\<^enum> the "inner-syntax" (i.e. the syntax for @{term \<open>\<Lambda>\<close>}-terms) 
   with an evolved, eight-layer parsing and pretty-printing process
-  based on an Early-algorithm.
+  based on an Earley-algorithm.
 \<close>
 
 text\<open>This picture is less and less true for a number of reasons:
-\<^enum> With the advent of \<open>(\<open>)... (\<close>)\<close>, a mechanism for
-  \<^emph>\<open>cascade-syntax\<close> came to the Isabelle platform that introduce a flexible means
+\<^enum> With the advent of \<open>\<open> ... \<close>\<close>, a mechanism for
+  \<^emph>\<open>cascade-syntax\<close> came to the Isabelle platform that introduces a flexible means
   to change parsing contexts \<^emph>\<open>and\<close> parsing technologies. 
 \<^enum> Inside the term-parser levels, the concept of \<^emph>\<open>cartouche\<close> can be used 
   to escape the parser and its underlying parsing technology.
 \<^enum> Outside, in the traditional toplevel-parsers, the 
-  \<open>(\<open>)... (\<close>)\<close> is becoming more and more enforced
+  \<open>\<open> ... \<close>\<close> is becoming more and more enforced
   (some years ago, syntax like \<open>term{* ... *}\<close> was replaced by 
-   syntax \<open>term(\<open>)... (\<close>)\<close>. This makes technical support of cascade syntax
+   syntax \<open>term\<open> ... \<close>\<close>. This makes technical support of cascade syntax
    more and more easy.
 \<^enum> The Lexer infra-structure is already rather generic; nothing prevents to
   add beside the lexer - configurations for ML-Parsers, Toplevel Command Syntax 
@@ -1474,8 +1486,8 @@ section\<open>Basics: string, bstring and xstring\<close>
 text\<open>\<^ML_type>\<open>string\<close> is the basic library type from the SML library
   in structure \<^ML_structure>\<open>String\<close>. Many Isabelle operations produce
   or require formats thereof introduced as type synonyms 
-  \<^ML_type>\<open>bstring\<close> (defined in structure  \<^ML_structure>\<open>Binding\<close>
-  and \<^ML_type>\<open>xstring\<close> (defined in structure \<^ML_structure>\<open>Name_Space\<close>.
+  \<^ML_type>\<open>bstring\<close> (defined in structure  \<^ML_structure>\<open>Binding\<close>)
+  and \<^ML_type>\<open>xstring\<close> (defined in structure \<^ML_structure>\<open>Name_Space\<close>).
   Unfortunately, the abstraction is not tight and combinations with 
   elementary routines might produce quite crappy results.\<close>
 
@@ -1486,7 +1498,7 @@ text\<open>... produces the system output \<^verbatim>\<open>val it = "here": bs
 ML\<open>String.explode b\<close> (* is harmless, but  *)
 ML\<open>String.explode(Binding.name_of
           (Binding.conglomerate[Binding.qualified_name "X.x", @{binding "here"}]  ))\<close>
-text\<open>... whioch leads to the output \<^verbatim>\<open>val it = [#"x", #"_", #"h", #"e", #"r", #"e"]: char list\<close>\<close>
+text\<open>... which leads to the output \<^verbatim>\<open>val it = [#"x", #"_", #"h", #"e", #"r", #"e"]: char list\<close>\<close>
 
 text\<open> However, there is an own XML parser for this format. See Section Markup. \<close>
 
@@ -1519,11 +1531,11 @@ text\<open>The structures @{ML_structure Markup} and @{ML_structure Properties}
   annotation data which is part of the protocol sent from Isabelle to the front-end.
   They are qualified as "quasi-abstract", which means they are intended to be an abstraction of 
   the serialized, textual presentation of the protocol. Markups are structurally a pair of a key
-  and properties; @{ML_structure Markup} provides a number of of such \<^emph>\<open>key\<close>s for annotation classes
+  and properties; @{ML_structure Markup} provides a number of such \<^emph>\<open>key\<close>s for annotation classes
   such as "constant", "fixed", "cartouche", some of them quite obscure. Here is a code sample
   from \<^theory_text>\<open>Isabelle_DOF\<close>. A markup must be tagged with an id; this is done by the @{ML serial}-function
-  discussed earlier. Markup Operations, were used for hyperlinking applications to binding
-  occurrences, info for hovering, infors for type ... \<close>  
+  discussed earlier. Markup operations were used for hyperlinking applications to binding
+  occurrences, info for hovering, infos for type ... \<close>  
 ML\<open>
 (* Position.report is also a type consisting of a pair of a position and markup. *)
 (* It would solve all my problems if I find a way to infer the defining Position.report
@@ -1546,7 +1558,7 @@ fun theory_markup (def:bool) (name:string) (id:serial) (pos:Position.T) =
       (Markup.entity Markup.theoryN name);
 Markup.theoryN : string;
 
-serial();   (* A global, lock-guarded seriel counter used to produce unique identifiers,
+serial();   (* A global, lock-guarded serial counter used to produce unique identifiers,
                be it on the level of thy-internal states or as reference in markup in
                PIDE *)
 \<close>
@@ -1583,7 +1595,7 @@ text\<open>The @\<open>ML report_defining_occurrence\<close>-function above take
 
 subsection\<open>A Slightly more Complex Example\<close>
 text\<open>Note that this example is only animated in the integrated source of this document;
-     it is essential that is executed inside Isabelle/jedit. \<close>
+     it is essential that is executed inside Isabelle/jEdit. \<close>
 ML \<open>
 
 fun markup_tvar def_name ps (name, id) =
@@ -1752,7 +1764,7 @@ text\<open>Parsing Combinators go back to monadic programming as advocated by Wa
       'a * (Context.generic * Token.T list)\<close>
 
   Since the semantics of an Isabelle command is a \<^ML_type>\<open>Toplevel.transition -> Toplevel.transition \<close>
-  or theory  \<^ML_type>\<open>theory -> theory\<close>  function, i.e. a global system transition.
+  or theory  \<^ML_type>\<open>theory -> theory\<close>  function, i.e. a global system transition,
   "parsers" of that type can be constructed and be bound as call-back functions
   to a table in the Toplevel-structure of Isar.
   
@@ -1772,7 +1784,7 @@ text\<open>Parsing Combinators go back to monadic programming as advocated by Wa
 \<^item> \<^ML>\<open>op |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e\<close> 
   concatenate and forget first parse result
 \<^item> \<^ML>\<open>op --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e\<close> 
-  concatenation and forget second parse result
+  concatenate and forget second parse result
 \<^item> \<^ML>\<open>op ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c\<close> 
 \<^item> \<^ML>\<open>op ::: : ('a -> 'b * 'c) * ('c -> 'b list * 'd) -> 'a -> 'b list * 'd\<close> 
 \<^item> \<^ML>\<open>op @@@ : ('a -> 'b list * 'c) * ('c -> 'b list * 'd) -> 'a -> 'b list * 'd\<close> 
@@ -1791,7 +1803,7 @@ fun parser2contextparser pars (ctxt, toks) = let val (a, toks') = pars toks
                                              in  (a,(ctxt, toks')) end;
 val _ = parser2contextparser : 'a parser -> 'a context_parser;
 
-(* bah, is the same as Scan.lift *)
+(* bah, it's the same as Scan.lift *)
 val _ = Scan.lift Args.cartouche_input : Input.source context_parser;\<close>
 
 subsection\<open>Advanced Parser Library\<close>
@@ -1804,10 +1816,10 @@ text\<open>There are two parts. A general multi-purpose parsing combinator libra
 \<^item> \<^ML>\<open>Parse.nat: int parser\<close>  
 \<^item> \<^ML>\<open>Parse.int: int parser\<close>
 \<^item> \<^ML>\<open>Parse.enum_positions: string -> 'a parser -> ('a list * Position.T list) parser\<close>
-\<^item> \<^ML>\<open>Parse.enum: string -> 'a parser -> 'a list parser\<close>
+\<^item> \<^ML>\<open>Parse.enum : string -> 'a parser -> 'a list parser\<close>
 \<^item> \<^ML>\<open>Parse.input: 'a parser -> Input.source parser\<close>
 
-\<^item> \<^ML>\<open>Parse.enum : string -> 'a parser -> 'a list parser\<close>
+\<^item> \<^ML>\<open>Parse.enum': string -> 'a context_parser -> 'a list context_parser\<close>
 \<^item> \<^ML>\<open>Parse.!!! : (Token.T list -> 'a) -> Token.T list -> 'a\<close>
 \<^item> \<^ML>\<open>Parse.position: 'a parser -> ('a * Position.T) parser\<close>
 
@@ -1816,7 +1828,7 @@ text\<open>There are two parts. A general multi-purpose parsing combinator libra
 
 text\<open>The second part is much more high-level, and can be found under \<^ML_structure>\<open>Args\<close>.
   In parts, these combinators are again based on more low-level combinators, in parts they serve as 
-  an an interface to the underlying Earley-parser for mathematical notation used in types and terms.
+  an interface to the underlying Earley-parser for mathematical notation used in types and terms.
   This is perhaps meant with the fairly cryptic comment:
   "Quasi-inner syntax based on outer tokens: concrete argument syntax of
   attributes, methods etc." at the beginning of this structure.\<close>
@@ -1919,7 +1931,7 @@ subsubsection\<open> Example \<close>
 text\<open>Since this is so common in interface programming, there are a number of antiquotations\<close>
 ML\<open>
 val H = @{binding here}; (* There are "bindings" consisting of a text-span and a position, 
-                            where \<dieresis>positions\<dieresis> are absolute references to a file *)                                  
+                            where "positions" are absolute references to a file *)                                  
 
 Binding.pos_of H;  (* clicking on "H" activates the hyperlink to the defining occ of "H" above *)
 (*  {offset=23, end_offset=27, id=-17214}: Position.T *)
@@ -1941,7 +1953,7 @@ subsubsection \<open>Example :Input streams. \<close>
 
 ML\<open> Input.source_explode (Input.string " f @{thm refl}");
   
-   (* If stemming from the input window, this can be s th like: 
+   (* If stemming from the input window, this can be something like: 
       
         [(" ", {offset=14, id=-2769}), ("f", {offset=15, id=-2769}), (" ", {offset=16, id=-2769}),
         ("@", {offset=17, id=-2769}), ("{", {offset=18, id=-2769}), ("t", {offset=19, id=-2769}),
@@ -1955,17 +1967,17 @@ ML\<open> Input.source_explode (Input.string " f @{thm refl}");
 
 section\<open>Term Parsing\<close>  
 
-text\<open>The heart of the parsers for mathematical notation, based on an Earley parser that can cope
+text\<open>The heart of the parsers for mathematical notation, based on an Earley-parser that can cope
   with incremental changes of the grammar as required for sophisticated mathematical output, is hidden
   behind the API described in this section.\<close>
   
-text\<open> Note that the naming underlies the following convention : 
-   there are:
+text\<open> Note that the naming underlies the following convention. 
+   There are:
    \<^enum> "parser"s 
    \<^enum>  type-"checker"s, which usually also englobe the markup generation for PIDE
    \<^enum> "reader"s which do both together with pretty-printing
    
-   This is encapsulated the data structure @{ML_structure Syntax} --- 
+   This is encapsulated in the data structure @{ML_structure Syntax} --- 
    the table with const symbols,  print and ast translations, ... The latter is accessible, e.g. 
    from a Proof context via @{ML Proof_Context.syn_of}.
 \<close>
@@ -2096,7 +2108,7 @@ text\<open>The heart of the LaTeX generator is to be found in the structure \<^M
 This is an own parsing and writing process, with the risc that a parsed file in the IDE parsing
 process can not be parsed for the LaTeX Generator. The reason is twofold:
 
-\<^enum> The LaTeX Generator makes a rough attempt to mimic the LayOut if the thy-file; thus, its
+\<^enum> The LaTeX Generator makes a rough attempt to mimic the LayOut in the thy-file; thus, its
   spacing is relevant.
 \<^enum> there is a special bracket \<open>(*<*)\<close> ... \<open>(*>*)\<close> that allows to specify input that is checked by
   Isabelle, but excluded from the LaTeX generator (this is handled in an own sub-parser

install

@@ -181,6 +181,7 @@ install_and_register(){
     cp $GEN_DIR/scripts/* "$DIR"
     cp $GEN_DIR/document-templates/* "$DIR"
     cp $GEN_DIR/DOF/*/*.sty "$DIR"
+    cp $GEN_DIR/DOF/*/*.cls "$DIR"
     
     ISABELLE_SHORT_VERSION=`echo $ISABELLE_VERSION | sed -e 's/:.*$//'`
     sed -i -e "s|%%% CONFIG %%%| \
@@ -226,7 +227,7 @@ install_and_register(){
 }
 
 
-ISABELLE=`which isabelle`
+ISABELLE=`command -v isabelle`
 SKIP="false"
 while [ $# -gt 0 ]
 do

src/DOF/Isa_COL.thy

@@ -241,10 +241,47 @@ setup\<open>\<close>
 section\<open>Tables\<close>
 (* TODO ! ! ! *)
 (* dito the future monitor: table - block *)
+(* some studies *)
 
 
+ML\<open>
+local
+
+fun mk_line st1 st2 [a] =  [a @ [Latex.string st2]]
+   |mk_line st1 st2 (a::S) = [a @ [Latex.string st1]] @ mk_line st1 st2 S;
+
+fun table_antiquotation name =
+  Thy_Output.antiquotation_raw_embedded name 
+    (Scan.repeat1(Scan.repeat1(Scan.lift Args.cartouche_input)))
+    (fn ctxt => 
+      (fn content:Input.source list list =>
+          let fun check _ = ()  (* ToDo *)
+              val _  = check content
+          in  content 
+              |> (map(map (Thy_Output.output_document ctxt {markdown = false})
+                  #> mk_line "&" "\\\\"
+                  #> List.concat )
+                  #> List.concat)
+              |> Latex.enclose_block "\\table[allerhandquatsch]{" "}"
+          end
+      )
+    );
+
+in
+
+val _ =
+  Theory.setup (table_antiquotation \<^binding>\<open>table_inline\<close> );
+
+end
+\<close>
+
 section\<open>Tests\<close>
-   
+(*<*)
+text\<open> @{table_inline [display]
+          \<open>\<open>\<open>dfg\<close>\<open>dfg\<close>\<open>dfg\<close>\<close>
+           \<open>\<open>1\<close>  \<open>2\<close>  \<open>3\<close>\<close>
+          \<close>}\<close>
+(*>*)
 ML\<open>@{term "side_by_side_figure"};
    @{typ "doc_class rexp"}; 
    DOF_core.SPY;\<close>

src/DOF/RegExpInterface.thy

@@ -68,13 +68,13 @@ This universe of denotations is in our concrete case:\<close>
 
 text\<open>Now the denotational semantics for regular expression can be defined on a post-card:\<close>
 
-fun       L :: "'a rexp => 'a lang"
-  where   L_Emp :   "L Zero        = {}"
-         |L_One:    "L One         = {[]}"
-         |L_Atom:   "L (\<lfloor>a\<rfloor>)       = {[a]}"
-         |L_Un:     "L (el || er)  = (L el) \<union> (L er)"
-         |L_Conc:   "L (el ~~ er)  = {xs@ys | xs ys. xs \<in> L el \<and> ys \<in> L er}"
-         |L_Star:   "L (Star e)    = Regular_Set.star(L e)"
+fun       Lang :: "'a rexp => 'a lang"
+  where   L_Emp :   "Lang Zero        = {}"
+         |L_One:    "Lang One         = {[]}"
+         |L_Atom:   "Lang (\<lfloor>a\<rfloor>)       = {[a]}"
+         |L_Un:     "Lang (el || er)  = (Lang el) \<union> (Lang er)"
+         |L_Conc:   "Lang (el ~~ er)  = {xs@ys | xs ys. xs \<in> Lang el \<and> ys \<in> Lang er}"
+         |L_Star:   "Lang (Star e)    = Regular_Set.star(Lang e)"
 
 
 text\<open>A more useful definition is the sub-language - definition\<close>
@@ -152,6 +152,7 @@ text\<open>Here comes the hic : The reflection of the HOL-Automata module into a
 with an abstract interface hiding some generation artefacts like the internal states 
 of the deterministic automata ...\<close>
 
+
 ML\<open> 
 
 structure RegExpInterface : sig

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

@@ -0,0 +1,94 @@
+%% Copyright (c) 2019-2022 University of Exeter
+%%               2018-2022 University of Paris-Saclay
+%%               2018-2019 The University of Sheffield
+%%
+%% License:
+%%   This program can be redistributed and/or modified under the terms
+%%   of the LaTeX Project Public License Distributed from CTAN
+%%   archives in directory macros/latex/base/lppl.txt; either
+%%   version 1.3c of the License, or (at your option) any later version.
+%%   OR
+%%   The 2-clause BSD-style license.
+%%
+
+%%   2022/01/25 Unreleased/Isabelle2021
+
+%% Warning: Do Not Edit!
+%% =====================
+%% This is the root file for the Isabelle/DOF using the lipics class.
+%% Note that lipics cannot be distributed as part of Isabelle/DOF; you need
+%% to download lipics.cls from 
+%% https://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/
+%% and add it manually to the praemble.tex and the ROOT file.
+%%
+%% All customization and/or additional packages should be added to the file
+%% preamble.tex.
+
+\documentclass[a4paper,UKenglish,cleveref, autoref,thm-restate]{lipics-v2021-dof}
+\bibliographystyle{plainurl}% the mandatory bibstyle
+\usepackage{isabelle}
+\usepackage{isabellesym}
+% \usepackage{amsmath}
+% \usepackage{DOF-amssymb}
+\usepackage[numbers, sort&compress, sectionbib]{natbib}
+\IfFileExists{DOF-core.sty}{}{%
+  \PackageError{DOF-core}{Isabelle/DOF not installed. 
+    This is a Isabelle_DOF project. The document preparation requires
+    the Isabelle_DOF framework. Please obtain the framework by cloning
+    the Isabelle_DOF git repository, i.e.: 
+         "git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
+    You can install the framework as follows:
+         "cd Isabelle_DOF/document-generator && ./install"}{%
+    For further help, see https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF}
+}
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% provide an alternative definition of 
+% begin: scholarly_paper.author
+\RequirePackage{keycommand}
+\makeatletter
+\newcommand{\DOFlipicsAuthor}[4]{\expandafter\author{#1}{#2}{#3}{#4}}
+\expandafter\newkeycommand\csname isaDof.text.scholarly_paper.author\endcsname%
+[label=,type=%
+,scholarly_paper.author.email=%
+,scholarly_paper.author.affiliation=%
+,scholarly_paper.author.orcid=%
+,scholarly_paper.author.http_site=%
+][1]{%
+  \protected@write\@auxout{}{\string\protect\string\DOFlipicsAuthor{#1}%
+                                           {\commandkey{scholarly_paper.author.affiliation}}
+         {\commandkey{scholarly_paper.author.email}}
+        {\commandkey{scholarly_paper.author.orcid}}
+        {}
+        }
+}
+
+\makeatother
+% end: scholarly_paper.author
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\input{ontologies}
+\renewcommand{\DOFauthor}{}
+\renewcommand{\DOFinstitute}{}
+\expandafter\newcommand\csname 2authand\endcsname{}
+\expandafter\newcommand\csname 3authand\endcsname{}
+\expandafter\newcommand\csname 4authand\endcsname{}
+
+\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
+\begin{document}
+
+
+\maketitle
+\input{session}
+% optional bibliography
+\IfFileExists{root.bib}{%
+{\small  
+  \bibliography{root}
+}}{}
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:

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

@@ -0,0 +1,106 @@
+%% Copyright (c) 2019-2021 University of Exeter
+%%               2018-2021 University of Paris-Saclay
+%%               2018-2019 The University of Sheffield
+%%
+%% License:
+%%   This program can be redistributed and/or modified under the terms
+%%   of the LaTeX Project Public License Distributed from CTAN
+%%   archives in directory macros/latex/base/lppl.txt; either
+%%   version 1.3c of the License, or (at your option) any later version.
+%%   OR
+%%   The 2-clause BSD-style license.
+%%
+%%   SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
+
+%%   2021/03/22 Unreleased/Isabelle2021
+
+%% Warning: Do Not Edit!
+%% =====================
+%% This is the root file for the Isabelle/DOF using the scrartcl class.
+%%
+%% All customization and/or additional packages should be added to the file
+%% preamble.tex.
+
+\RequirePackage{ifvtex}
+\RequirePackage{fix-cm}
+\documentclass[]{svjour3}
+\usepackage[T1]{fontenc}
+\usepackage[utf8]{inputenc}
+\usepackage{mathptmx}
+\bibliographystyle{abbrvnat}
+\usepackage[USenglish]{babel}
+\usepackage{isabelle}
+\usepackage{xcolor}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{DOF-amssymb}
+\usepackage[numbers, sort&compress, sectionbib]{natbib}
+\IfFileExists{DOF-core.sty}{}{%
+  \PackageError{DOF-core}{Isabelle/DOF not installed. 
+    This is a Isabelle_DOF project. The document preparation requires
+    the Isabelle_DOF framework. Please obtain the framework by cloning
+    the Isabelle_DOF git repository, i.e.: 
+         "git clone <isadofurl>"
+    You can install the framework as follows:
+         "cd Isabelle_DOF/document-generator && ./install"}{%
+    For further help, see <isadofurl>}
+}
+\input{ontologies}
+\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
+\usepackage{graphicx}
+\usepackage{hyperref}
+\setcounter{tocdepth}{3} 
+\hypersetup{%
+   bookmarksdepth=3
+  ,pdfpagelabels
+  ,pageanchor=true
+  ,bookmarksnumbered
+  ,plainpages=false
+} % more detailed digital TOC (aka bookmarks)
+\sloppy
+\allowdisplaybreaks[4]
+\urlstyle{rm}
+\isabellestyle{it}
+\usepackage[caption]{subfig}
+\usepackage[size=footnotesize]{caption}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%% Overrides the (rightfully issued) warning by Koma Script that \rm
+%%% etc. should not be used (they are deprecated since more than a
+%%% decade)
+  \DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
+  \DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
+  \DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
+  \DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
+  \DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{document}
+\selectlanguage{USenglish}%
+\renewcommand{\bibname}{References}%
+\renewcommand{\figurename}{Fig.}
+\renewcommand{\abstractname}{Abstract.}
+\renewcommand{\subsubsectionautorefname}{Sect.}
+\renewcommand{\subsectionautorefname}{Sect.}
+\renewcommand{\sectionautorefname}{Sect.}
+\renewcommand{\figureautorefname}{Fig.}
+\newcommand{\subtableautorefname}{\tableautorefname}
+\newcommand{\subfigureautorefname}{\figureautorefname}
+\newcommand{\lstnumberautorefname}{Line}
+
+
+
+\maketitle
+\input{session}
+% optional bibliography
+\IfFileExists{root.bib}{%
+{\small  
+  \newcommand{\urlprefix}{}
+  \bibliography{root}
+}}{}
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:

src/ontologies/CENELEC_50128/CENELEC_50128.thy

@@ -319,7 +319,7 @@ section\<open>Objectives, Conformance and Software Integrity Levels\<close>
 
 datatype sil = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
 
-type_synonym saftety_integraytion_level = sil
+type_synonym safety_integration_level = sil
 
 
 doc_class objectives =
@@ -373,10 +373,6 @@ doc_class FnI = requirement +
    is_concerned :: "role set" <= "UNIV"    
    type_synonym functions_and_interfaces = FnI
 
-doc_class AC = requirement +
-   is_concerned :: "role set" <= "UNIV" 
-
-type_synonym application_conditions = AC
 
 text\<open>The category \<^emph>\<open>assumption\<close> is used for domain-specific assumptions. It has formal, semi-formal 
       and informal sub-categories. They have to be  tracked and discharged by appropriate 
@@ -387,6 +383,12 @@ datatype ass_kind = informal | semiformal | formal
 doc_class assumption = requirement +
      assumption_kind :: ass_kind <= informal 
 
+doc_class AC = assumption +
+   is_concerned :: "role set" <= "UNIV" 
+
+type_synonym application_conditions = AC
+
+
 text\<open> The category \<^emph>\<open>exported constraint\<close> (or \<^emph>\<open>EC\<close>  for short) is used for formal application 
 conditions; They represent in particular \<^emph>\<open>derived constraints\<close>, i.e. constraints that arrive
 as side-conditions during refinement proofs or implementation decisions and must be tracked.\<close>

src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty

@@ -71,6 +71,7 @@
 ,CENELEC_50128.SRAC.formal_repr=%
 ,CENELEC_50128.SRAC.assumption_kind=%
 ,CENELEC_50128.EC.assumption_kind=%
+,CENELEC_50128.assumption.assumption_kind=%
 ][1]{%
   \begin{isamarkuptext}%
       \ifthenelse{\equal{\commandkey{CENELEC_50128.requirement.long_name}}{}}{%
@@ -123,6 +124,7 @@
 ,CENELEC_50128.SRAC.formal_repr=%
 ,CENELEC_50128.SRAC.assumption_kind=%
 ,CENELEC_50128.EC.assumption_kind=%
+,CENELEC_50128.assumption.assumption_kind=%
 ][1]{%
   \begin{isamarkuptext}%
       \ifthenelse{\equal{\commandkey{CENELEC_50128.requirement.long_name}}{}}{%

src/ontologies/Conceptual/Conceptual.thy

@@ -11,6 +11,8 @@
  *   SPDX-License-Identifier: BSD-2-Clause
  *************************************************************************)
 
+section\<open>A conceptual introduction into DOF and its features:\<close>
+
 theory Conceptual
   imports "../../DOF/Isa_DOF" "../../DOF/Isa_COL"
 begin
@@ -18,7 +20,61 @@ begin
 
 doc_class A =
    level :: "int option"
-   x :: int  
+   x :: int
+
+subsection\<open>Excursion: On the semantic consequences of this definition: \<close>
+
+text\<open>This class definition leads an implicit Isabelle/HOL  \<^theory_text>\<open>record\<close>  definition 
+(cf. \<^url>\<open>https://isabelle.in.tum.de/dist/Isabelle2021/doc/isar-ref.pdf\<close>, chapter 11.6.).
+Consequently, \<^theory_text>\<open>doc_class\<close>'es inherit the entire theory-infrastructure from Isabelle records:
+\<^enum> there is a HOL-type \<^typ>\<open>A\<close> and its extensible version \<^typ>\<open>'a A_scheme\<close> 
+\<^enum> there are HOL-terms representing \<^emph>\<open>doc_class instances\<close> with the high-level syntax:
+    \<^enum> \<^term>\<open>undefined\<lparr>level := Some (1::int), x := 5::int \<rparr> :: A\<close>
+      (Note that this way to construct an instance is not necessarily computable
+    \<^enum> \<^term>\<open>\<lparr>tag_attribute = X, level = Y, x = Z\<rparr> :: A\<close>
+    \<^enum> \<^term>\<open>\<lparr>tag_attribute = X, level = Y, x = Z, \<dots> = M\<rparr> :: ('a A_scheme)\<close>
+\<^enum> there is an entire proof infra-structure allowing to reason about \<^emph>\<open>doc_class instances\<close>;
+  this involves the constructor, the selectors (representing the  \<^emph>\<open>attributes\<close> in OO lingo)
+  the update functions, the rules to establish equality and, if possible the code generator
+  setups:
+    \<^enum> \<^term>\<open>A.make :: int \<Rightarrow> int option \<Rightarrow> int \<Rightarrow> A\<close>
+    \<^enum> \<^term>\<open>A.level :: 'a A_scheme \<Rightarrow> int option\<close>
+    \<^enum> \<^term>\<open>A.level_update :: (int option \<Rightarrow> int option) \<Rightarrow> 'a A_scheme \<Rightarrow> 'a A_scheme\<close>
+    \<^enum> ...
+  together with the rules such as:
+    \<^enum> @{thm [display] A.simps(2)}
+    \<^enum> @{thm [display] A.simps(6)}
+    \<^enum> ...
+\<close>
+(* the generated theory of the \<^theory_text>\<open>doc_class\<close> A can be inspected, of course, by *)
+find_theorems (60) name:Conceptual name:A
+
+
+text\<open>As a consequence of the theory of the \<^theory_text>\<open>doc_class\<close> \<open>A\<close>, the code-generator setup lets us 
+evaluate statements such as: \<close>
+
+value\<open> the(A.level (A.make 3 (Some 4) 5)) = 4\<close>
+
+text\<open>And finally, as a consequence of the above semantic construction of \<^theory_text>\<open>doc_class\<close>'es, the internal
+\<open>\<lambda>\<close>-calculus representation of class instances looks as follows:\<close>
+
+ML\<open>
+val tt = @{term \<open>the(A.level (A.make 3 (Some 4) 5))\<close>}
+\<close>
+
+text\<open>For the code-generation, we have the following access to values representing class instances:\<close>
+ML\<open>
+val A_make = @{code A.make};
+val zero   = @{code "0::int"};
+val one    = @{code "1::int"};
+val add    = @{code "(+) :: int \<Rightarrow> int \<Rightarrow> int"};
+
+A_make zero (SOME one) (add one one)
+\<close>
+
+
+subsection\<open>An independent class-tree root: \<close>
+
 
 doc_class B =
    level :: "int option"
@@ -29,13 +85,17 @@ doc_class B =
 text\<open>We may even use type-synonyms for class synonyms ...\<close>
 type_synonym XX = B
 
+
+subsection\<open>Examples of inheritance \<close>
+
 doc_class C = XX +                           
    z :: "A option"             <= None      (* A LINK, i.e. an attribute that has a type
                                                referring to a document class. Mathematical
                                                relations over document items can be modeled. *)
-   g :: "thm"
+   g :: "thm"                               (* a reference to the proxy-type 'thm' allowing
+                                               to denote references to theorems inside attributes *)
 
-datatype enum = X1 | X2 | X3
+datatype enum = X1 | X2 | X3                (* we add an enumeration type ... *)
    
 doc_class D = B +
    x  :: "string"              <= "\<open>def \<longrightarrow>\<close>" (* overriding default *)
@@ -57,15 +117,44 @@ doc_class F  =
    b           :: "(A \<times> C) set"  <= "{}"       (* This is a relation link, roughly corresponding
                                                  to an association class. It can be used to track
                                                  claims to result - relations, for example.*) 
-   invariant b :: "\<lambda>\<sigma>::F. r \<sigma> \<noteq> [] \<and> card(b \<sigma>) \<ge> 3"
-        and  c :: "\<lambda>\<sigma>::F. properties \<sigma> \<noteq> []"
+   b'          :: "(A \<times> C) list"  <= "[]"
+   invariant br :: "r \<sigma> \<noteq> [] \<and> card(b \<sigma>) \<ge> 3"
+        and  br':: "r \<sigma> \<noteq> [] \<and> length(b' \<sigma>) \<ge> 3"
+        and  cr :: "properties \<sigma> \<noteq> []"
+
+text\<open>The effect of the invariant declaration is to provide intern definitions for validation 
+functions of this invariant. They can be referenced as follows:\<close>
+thm br_inv_def
+thm br'_inv_def
+thm cr_inv_def
+
+term "\<lparr>F.tag_attribute = 5, properties = [], r = [], u = undefined, s = [], b = {}, b' = []\<rparr>"
+
+term "br' (\<lparr>F.tag_attribute = 5, properties = [], r = [], u = undefined, s = [], b = {}, b' = []\<rparr>) "
+
+text\<open>Now, we can use these definitions in order to generate code for these validation functions.
+Note, however, that not everything that we can write in an invariant (basically: HOL) is executable,
+or even compilable by the code generator setup:\<close>
+
+ML\<open> val cr_inv_code = @{code "cr_inv"} \<close> \<comment> \<open>works albeit thm is abstract ...\<close>
+text\<open>while in :\<close>
+(* ML\<open> val br_inv_code = @{code "br_inv"} \<close> \<comment>\<open>this does not work ...\<close> *)
+
+text\<open>... the compilation fails due to the fact that nothing prevents the user 
+     to define an infinite relation between \<^typ>\<open>A\<close> and  \<^typ>\<open>C\<close>. However, the alternative
+variant: \<close>
+
+ML\<open> val br'_inv_code = @{code "br'_inv"} \<close> \<comment> \<open>does work ...\<close>
+
+text\<open>... is compilable ...\<close>
+
 
 
 doc_class G = C +
    g :: "thm"  <= "@{thm \<open>HOL.refl\<close>}"
 
 doc_class M = 
-   trace :: "(A + C + D + F) list"
+   ok :: "unit"
    accepts "A ~~ \<lbrace>C || D\<rbrace>\<^sup>* ~~ \<lbrakk>F\<rbrakk>"
 
 
@@ -76,11 +165,13 @@ ML\<open> Session.get_keywords(); (* this looks to be really session global. *)
 ML\<open> Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \<close>
 *)
 
+open_monitor*[aaa::M]
 section*[test::A]\<open>Test and Validation\<close>
+term\<open>Conceptual.M.make\<close>
 text\<open>Defining some document elements to be referenced in later on in another theory: \<close>
 text*[sdf]\<open> Lorem ipsum @{thm refl}\<close> 
 text*[ sdfg :: F] \<open> Lorem ipsum @{thm refl}\<close>  
 text*[ xxxy ] \<open> Lorem ipsum @{F \<open>sdfg\<close>} rate @{thm refl}\<close>  
-
+close_monitor*[aaa]
 
 end     

src/ontologies/scholarly_paper/DOF-scholarly_paper.sty

@@ -14,7 +14,7 @@
 
 \NeedsTeXFormat{LaTeX2e}\relax
 \ProvidesPackage{DOF-scholarly_paper}
-  [<isadofltxversion>%
+  [2021/03/22 Unreleased/Isabelle2021%
   Document-Type Support Framework for Isabelle (LNCS).]
 
 \RequirePackage{DOF-COL}
@@ -40,7 +40,7 @@
       \RequirePackage{DOF-scholarly_paper-thm}%
     }%
     {%
-      \@ifclassloaded{lipics-v2019}%
+      \@ifclassloaded{lipics-v2021-dof}%
       {%
         \newcommand{\institute}[1]{}%
         \newcommand{\inst}[1]{}%
@@ -48,15 +48,30 @@
         \newcommand{\email}[1]{}%
       }%
       {%
-        \@ifclassloaded{eptcs}%
+        \@ifclassloaded{lipics-v2019}%
         {%
+          \newcommand{\institute}[1]{}%
           \newcommand{\inst}[1]{}%
           \newcommand{\orcidID}[1]{}%
+          \newcommand{\email}[1]{}%
         }%
         {%
-          \PackageError{DOF-scholarly_paper}
-                       {Scholarly Paper only supports LNCS or scrartcl as document class.}
-                       {}\stop%
+          \@ifclassloaded{eptcs}%
+          {%
+            \newcommand{\inst}[1]{}%
+            \newcommand{\orcidID}[1]{}%
+          }%
+          {%
+            \@ifclassloaded{svjour3}%
+            {%
+                \newcommand{\inst}[1]{}%
+            }%
+            {%
+              \PackageError{DOF-scholarly_paper}
+                          {Scholarly Paper only supports LNCS or scrartcl as document class.}
+                          {}\stop%
+            }%
+          }%
         }%
       }%
     }

src/ontologies/scholarly_paper/scholarly_paper.thy

@@ -122,6 +122,11 @@ As Security of the system we define etc...
 A formal statement can, but must not have a reference to true formal Isabelle/Isar definition. 
 \<close>
 
+doc_class background = text_section +
+   comment :: string
+   claims  :: "thm list"
+
+
 subsection\<open>Technical Content and its Formats\<close>
 
 datatype status = formal | semiformal | description
@@ -137,7 +142,7 @@ doc_class technical = text_section +
    definition_list :: "string list" <=  "[]"
    status          :: status <= "description"
    formal_results  :: "thm list"
-   invariant L1    :: "\<lambda>\<sigma>::technical. the (level \<sigma>) > 0"
+   invariant L1    :: "the (level \<sigma>) > 0"
 
 type_synonym tc = technical (* technical content *)
 
@@ -186,8 +191,8 @@ doc_class math_content = tc +
    short_name    :: string <= "''''"
    status        :: status <= "semiformal"
    mcc           :: "math_content_class" <= "thm" 
-   invariant s1  :: "\<lambda> \<sigma>::math_content. \<not>referentiable \<sigma> \<longrightarrow> short_name \<sigma> = ''''"
-   invariant s2  :: "\<lambda> \<sigma>::math_content. status \<sigma> = semiformal"
+   invariant s1  :: "\<not>referentiable \<sigma> \<longrightarrow> short_name \<sigma> = ''''"
+   invariant s2  :: "technical.status \<sigma> = semiformal"
 type_synonym math_tc = math_content
 
 text\<open>The class \<^typ>\<open>math_content\<close> is perhaps more adequaltely described as "math-alike content".
@@ -236,27 +241,28 @@ text\<open>The key class definitions are motivated by the AMS style.\<close>
 doc_class "definition"  = math_content +
    referentiable :: bool <= True
    mcc           :: "math_content_class" <= "defn" 
-   invariant d1  :: "\<lambda> \<sigma>::definition. mcc \<sigma> = defn" (* can not be changed anymore. *)
+   invariant d1  :: "mcc \<sigma> = defn" (* can not be changed anymore. *)
+
 
 doc_class "theorem"     = math_content +
    referentiable :: bool <= True
    mcc           :: "math_content_class" <= "thm" 
-   invariant d2  :: "\<lambda> \<sigma>::theorem. mcc \<sigma> = thm"
+    invariant d2  :: "mcc \<sigma> = thm"
 
 doc_class "lemma"     = math_content +
    referentiable :: bool <= "True"
    mcc           :: "math_content_class" <= "lem" 
-   invariant d3  :: "\<lambda> \<sigma>::lemma. mcc \<sigma> = lem"
+   invariant d3  :: "mcc \<sigma> = lem"
 
 doc_class "corollary"     = math_content +
    referentiable :: bool <= "True"
    mcc           :: "math_content_class" <= "cor" 
-   invariant d4  :: "\<lambda> \<sigma>::corollary. mcc \<sigma> = thm"
+    invariant d4  :: "mcc \<sigma> = thm"
 
 doc_class "math_example"     = math_content +
    referentiable :: bool <= "True"
    mcc           :: "math_content_class" <= "expl" 
-   invariant d5  :: "\<lambda> \<sigma>::math_example. mcc \<sigma> = expl"
+   invariant d5  :: "mcc \<sigma> = expl"
 
 
 subsubsection\<open>Ontological Macros \<^verbatim>\<open>Definition*\<close> , \<^verbatim>\<open>Lemma**\<close>, \<^verbatim>\<open>Theorem*\<close> ... \<close>
@@ -465,6 +471,7 @@ doc_class article =
             \<lbrace>author\<rbrace>\<^sup>+         ~~ 
             abstract          ~~
             \<lbrace>introduction\<rbrace>\<^sup>+   ~~ 
+            \<lbrace>background\<rbrace>\<^sup>*     ~~ 
             \<lbrace>technical || example \<rbrace>\<^sup>+      ~~
             \<lbrace>conclusion\<rbrace>\<^sup>+     ~~  
             bibliography      ~~

src/scripts/build_lib.sh

@@ -119,6 +119,7 @@ fi
 cp $ROOT root.tex
 cp $ISABELLE_HOME_USER/DOF/latex/*.sty .
 cp $ISABELLE_HOME_USER/DOF/document-template/*.sty .
+cp $ISABELLE_HOME_USER/DOF/document-template/*.cls .
 
 # delete outdated aux files from previous runs
 rm -f *.aux 

src/tests/AssnsLemmaThmEtc.thy

@@ -69,8 +69,8 @@ different class. "F" and "assertion" have only in common that they posses the at
 \<^verbatim>\<open>property\<close>: \<close>
 
 text\<open>Creation just like that: \<close>
-assert*[aaa::assertion] "3 < (4::int)"
-assert*[aaa::assertion] "0 < (4::int)"
+assert*[ababa::assertion] "3 < (4::int)"
+assert*[ababa::assertion] "0 < (4::int)"
 
 
 end

src/tests/Attributes.thy

@@ -30,17 +30,52 @@ val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, moni
 Symtab.dest docitem_tab;
 Symtab.dest docclass_tab;
 \<close>
-
-
 ML\<open>
-fun fac x = if x = 0 then 1 else x * (fac(x -1));
-fac 3;
+#value(the(the(Symtab.lookup docitem_tab "aaa")))
+
 \<close>
 
-ML\<open>
-open Thm;
-\<close>
+find_theorems (60) name:"Conceptual.M." 
 
+value [simp]"trace(M.make undefined [] ())"
+value "ok(M.make undefined_AAA [] ())"
+value "trace(M.make undefined_AAA [] ())"
+value "tag_attribute(M.make undefined_AAA [] ())"
+
+
+value "ok(M.make 0 [] ())"
+(*
+value "ok(M.make undefined [] ())"
+value "ok(M.make 0 [] undefined)"
+*)
+
+value [simp] \<open> M.ok 
+                   (Conceptual.M.trace_update (\<lambda>x. [])
+                    (Conceptual.M.tag_attribute_update (\<lambda>x. 0)
+                     (Conceptual.M.ok_update (\<lambda>x. ())
+                   (undefined::M)) 
+                   ))\<close>
+
+value [simp] \<open> M.ok 
+                   (Conceptual.M.trace_update (\<lambda>x. [])
+                    (Conceptual.M.tag_attribute_update (\<lambda>x. 0)
+                     (Conceptual.M.ok_update (\<lambda>x. ())
+                   (undefined::M)) 
+                   ))\<close>
+value  \<open> M.ok 
+                   (Conceptual.M.trace_update (\<lambda>x. [])
+                    (Conceptual.M.tag_attribute_update (\<lambda>x. 0)
+                     (Conceptual.M.ok_update (\<lambda>x. ())
+                   (AAAA::M)) 
+                   ))\<close>
+
+
+value  \<open> M.ok 
+                   (Conceptual.M.trace_update (\<lambda>x. [])
+                    (Conceptual.M.tag_attribute_update (\<lambda>x. 0)
+                     (Conceptual.M.ok_update (\<lambda>x. ())
+                   (M.make XX1 XX2 XX3::M)) 
+                   ))\<close>
 
 
 text\<open>A text item containing standard theorem antiquotations and complex meta-information.\<close>
@@ -68,6 +103,8 @@ text*[omega::E, x = "''def''"]\<open> Lorem ipsum ... @{thm refl} \<close>
 text\<open> As mentioned in @{docitem \<open>dfgdfg\<close>} \<close>
 
 text\<open>Here is a simulation what happens on the level of the (HOL)-term representation:\<close>
+typ \<open>'a A_scheme\<close>
+typ \<open>A\<close>
 term "A.x (undefined\<lparr>A.x := 3\<rparr>)"
 term "B.x ((undefined::C)\<lparr>B.y := [''sdf'']\<rparr>)"
 term "C.z ((undefined::C)\<lparr>B.y := [''sdf''], z:= Some undefined\<rparr>)"

src/tests/Concept_Example_Low_Level_Invariant.thy

@@ -14,7 +14,7 @@
 chapter\<open>Setting and modifying attributes of doc-items\<close>
 
 theory 
-  Concept_ExampleInvariant
+  Concept_Example_Low_Level_Invariant
 imports 
   "Isabelle_DOF.Conceptual" (* we use the generic "Conceptual" ontology *)
 begin
@@ -58,7 +58,7 @@ subsection*[d::A, x = "4"] \<open> Lorem ipsum dolor sit amet, ... \<close>
 (* test : update should not fail, invariant still valid *)
 update_instance*[d::A, x += "1"]
 
-(* test : with the next step it should fail :
+(* test : with the next step it should fail : 
 update_instance*[d::A, x += "1"]
 *)
 
@@ -101,19 +101,20 @@ open_monitor*[struct::M]
 
 subsection*[a::A, x = "3"]       \<open> Lorem ipsum dolor sit amet, ... \<close>
 
-text*[c1::C, x = "''beta''"]  \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ...  \<close>
+text*[c1::C, x = "''beta''"]     \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ...  \<close>
 
-text*[d1::E, a1 = "X3"]       \<open> ... phasellus amet id massa nunc, pede suscipit repellendus, ... \<close>
+text*[d1::E, a1 = "X3"]          \<open> ... phasellus amet id massa nunc, pede suscipit repellendus, ... \<close>
     
-text*[c2:: C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium consectetuer...  \<close>
+text*[c2:: C, x = "''delta''"]   \<open> ... in ut tortor eleifend augue pretium consectetuer...  \<close>
 
 subsection*[f::E]                \<open> Lectus accumsan velit ultrices, ... }\<close>
 
 (*
-section*[f2::E]               \<open> Lectus accumsan velit ultrices, ... }\<close>
+section*[f2::E]                  \<open> Lectus accumsan velit ultrices, ... }\<close>
 *)
 
-ML\<open>val term = AttributeAccess.compute_attr_access (Context.Proof @{context}) "trace" "struct" @{here} @{here} ;
+ML\<open>val term = AttributeAccess.compute_attr_access 
+                  (Context.Proof @{context}) "trace" "struct" @{here} @{here} ;
    fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
    val string_pair_list = map conv (HOLogic.dest_list term)
   \<close>

src/tests/Evaluation.thy

@@ -0,0 +1,173 @@
+chapter\<open>Evaluation\<close>
+
+text\<open>Term Annotation Antiquotations (TA) can be evaluated with the help of the value* command.\<close>
+
+theory 
+  Evaluation
+imports 
+  "Isabelle_DOF-tests.TermAntiquotations"
+begin
+
+section\<open>\<^theory_text>\<open>ML*\<close>-Annotated SML-commands\<close>
+ML*[the_function::C,x=\<open>\<open>dfg\<close>\<close>]\<open>fun fac x = if x = 0 then 1 else x * fac(x-1);
+                               val t = @{const_name "List.Nil"}\<close>
+ML\<open>fac 5; t\<close> \<comment> \<open>this is a test that ML* is actually evaluated and the 
+                 resulting toplevel state is preserved.\<close>
+ML*\<open>3+4\<close>     \<comment> \<open>meta-args are optional\<close> 
+
+text\<open>... and here we reference @{B [display] \<open>the_function\<close>}.\<close>
+
+section\<open>\<^theory_text>\<open>value*\<close>-Annotated evaluation-commands\<close>
+
+
+text\<open>The value* command uses the same code as the value command
+and adds the possibility to evaluate Term Annotation Antiquotations (TA).
+For that an elaboration of the term referenced by a TA must be done before
+passing it to the evaluator.
+The current implementation is based on referential equality, syntactically, and
+with the help of HOL, on referential equivalence, semantically:
+Some built-ins remain as unspecified constants:
+\<^item> the docitem TA offers a way to check the reference of class instances
+  without checking the instances type.
+  It must be avoided for certification
+\<^item> the termrepr TA is left as unspecified constant for now.
+   A major refactoring of code should be done to enable
+  referential equivalence for termrepr, by changing the dependency
+  between the Isa_DOF theory and the Assert theory.
+  The assert_cmd function in Assert should use the value* command
+  functions, which make the elaboration of the term
+  referenced by the TA before passing it to the evaluator
+
+We also have the possibility to make some requests on classes instances, i.e. on docitems
+by specifying the doc_class.
+The TA denotes the HOL list of the values of the instances.
+The value of an instance is the record of every attributes of the instance.
+This way, we can use the usual functions on lists to make our request.
+
+The emphasis of this presentation is to present the evaluation possibilities and limitations
+of the current implementation.
+\<close>
+
+section\<open>Term Annotation evaluation\<close>
+
+text\<open>We can validate a term with TA:\<close>
+term*\<open>@{thm \<open>HOL.refl\<close>}\<close>
+
+text\<open>Now we can evaluate a term with TA:
+the current implementation return the term which references the object referenced by the TA.
+Here the evualuation of the TA will return the HOL.String which references the theorem:
+\<close>
+value*\<open>@{thm \<open>HOL.refl\<close>}\<close>
+
+value*[a::A]\<open>@{thm \<open>HOL.refl\<close>}\<close> (* using the option *)
+
+text\<open>An instance class is an object which allows us to define the concepts we want in an ontology.
+It is a concept which will be used to implement an ontology. It has roughly the same meaning as
+an individual in an OWL ontology.
+The validation process will check that the instance class @{docitem \<open>xcv1\<close>} is indeed
+an instance of the class @{doc_class A}:
+\<close>
+term*\<open>@{A \<open>xcv1\<close>}\<close>
+
+text\<open>The instance class @{docitem \<open>xcv1\<close>} is not an instance of the class @{doc_class B}:
+\<close>
+(* Error:
+term*\<open>@{B \<open>xcv1\<close>}\<close>*)
+
+text\<open>We can evaluate the instance class. The current implementation returns
+the value of the instance, i.e. a collection of every attribute of the instance: 
+\<close>
+value*\<open>@{A \<open>xcv1\<close>}\<close>
+
+text\<open>We can also get the value of an attribute of the instance:\<close>
+value*\<open>A.x @{A \<open>xcv1\<close>}\<close>
+
+text\<open>If the attribute of the instance is not initialized, we get an undefined value,
+whose type is the type of the attribute:\<close>
+term*\<open>level @{C \<open>xcv2\<close>}\<close>
+value*\<open>level @{C \<open>xcv2\<close>}\<close>
+
+text\<open>The value of a TA is the term itself:\<close>
+term*\<open>C.g @{C \<open>xcv2\<close>}\<close>
+value*\<open>C.g @{C \<open>xcv2\<close>}\<close>
+
+text\<open>Some terms can be validated, i.e. the term will be checked,
+and the existence of every object referenced by a TA will be checked,
+and can be evaluated by using referential equivalence.
+The existence of the instance @{docitem \<open>xcv4\<close>} can be validated,
+and the fact that it is an instance of the class @{doc_class F} } will be checked:\<close>
+term*\<open>@{F \<open>xcv4\<close>}\<close>
+
+text\<open>We can also evaluate the instance @{docitem \<open>xcv4\<close>}.
+The attribute \<open>b\<close> of the instance @{docitem \<open>xcv4\<close>} is of type @{typ "(A \<times> C) set"}
+but the instance @{docitem \<open>xcv4\<close>} initializes the attribute by using the \<open>docitem\<close> TA.
+Then the instance can be evaluate but only the references of the classes of the set
+used in the \<open>b\<close> attribute will be checked, and the type of these classes will not:
+\<close>
+value* \<open>@{F \<open>xcv4\<close>}\<close>
+
+text\<open>If we want the classes to be checked,
+we can use the TA which will also check the type of the instances.
+The instance @{A \<open>xcv3\<close>} is of type @{typ "A"} and the instance @{C \<open>xcv2\<close>} is of type @{typ "C"}:
+\<close>
+update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{C ''xcv2''})}"]
+
+text\<open>Using a TA in terms is possible, and the term is evaluated:\<close>
+value*\<open>[@{thm \<open>HOL.refl\<close>}, @{thm \<open>HOL.refl\<close>}]\<close>
+value*\<open>@{thm ''HOL.refl''} = @{thm (''HOL.refl'')}\<close>
+
+ML\<open>
+@{thm "refl"}
+\<close>
+
+section\<open>Request on instances\<close>
+
+text\<open>We define a new class Z:\<close>
+doc_class Z =
+  z::"int"
+
+text\<open>And some instances:\<close>
+text*[test1Z::Z, z=1]\<open>lorem ipsum...\<close>
+text*[test2Z::Z, z=4]\<open>lorem ipsum...\<close>
+text*[test3Z::Z, z=3]\<open>lorem ipsum...\<close>
+
+text\<open>We want to get all the instances of the @{doc_class Z}:\<close>
+value*\<open>@{Z-instances}\<close>
+
+text\<open>Now we want to get the instances of the @{doc_class Z} whose attribute z > 2:\<close>
+value*\<open>filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z-instances}\<close>
+
+text\<open>We can check that we have the list of instances we wanted:\<close>
+value*\<open>filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z-instances} = [@{Z \<open>test3Z\<close>}, @{Z \<open>test2Z\<close>}]
+       \<or> filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z-instances} = [@{Z \<open>test2Z\<close>}, @{Z \<open>test3Z\<close>}]\<close>
+
+text\<open>Now, we want to get all the instances of the @{doc_class A}\<close>
+value*\<open>@{A-instances}\<close>
+
+text\<open>Warning: If you make a request on attributes that are undefined in some instances,
+you will get a result which includes these unresolved cases.
+In the following example, we request the instances of the @{doc_class A}.
+But we have defined an instance @{docitem \<open>test\<close>} in theory @{theory Isabelle_DOF.Conceptual}
+whose our theory inherits from, and this docitem instance does not initialize its attribute \<^emph>\<open>x\<close>.
+So in the request result we get an unresolved case because the evaluator can not get
+the value of the \<^emph>\<open>x\<close> attribute of the instance @{docitem \<open>test\<close>}:\<close>
+value*\<open>filter (\<lambda>\<sigma>. A.x \<sigma> > 5) @{A-instances}\<close>
+
+section\<open>Limitations\<close>
+
+text\<open>There are still some limitations.
+The terms passed as arguments to the TA are not simplified and their evaluation fails:
+\<close>
+(* Error:
+value*\<open>@{thm (''HOL.re'' @ ''fl'')}\<close>
+value*\<open>@{thm ''HOL.refl''} = @{thm (''HOL.re'' @ ''fl'')}\<close>*)
+
+text\<open>The type checking is unaware that a class is subclass of another one.
+The @{doc_class "G"} is a subclass of the class @{doc_class "C"}, but one can not use it
+to update the instance @{docitem \<open>xcv4\<close>}:
+\<close>
+(* Error:
+update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{G ''xcv5''})}"]*)
+
+
+end

src/tests/High_Level_Syntax_Invariants.thy

@@ -0,0 +1,137 @@
+chapter\<open>High level syntax Invariants\<close>
+
+theory High_Level_Syntax_Invariants
+  imports "Isabelle_DOF.Isa_DOF"
+begin
+
+text\<open>
+  Ontological classes as described so far are too liberal in many situations.
+  There is a first high-level syntax implementation for class invariants.
+  These invariants can be checked when an instance of the class is defined.
+  To enable the checking of the invariants, the \<open>invariants_checking\<close>
+  theory attribute must be set:\<close>
+
+
+declare[[invariants_checking = true]]
+
+text\<open>For example, let's define the following two classes:\<close>
+
+doc_class class_inv1 =
+  int1 :: "int"
+  invariant inv1 :: "int1 \<sigma> \<ge> 3"
+
+doc_class class_inv2 = class_inv1 +
+  int2 :: "int"
+  invariant inv2 :: "int2 \<sigma> < 2"
+
+text\<open>The  symbol \<^term>\<open>\<sigma>\<close> is reserved and references the future instance class.
+  By relying on the implementation of the Records
+  in Isabelle/HOL~@{cite "wenzel:isabelle-isar:2020"},
+  one can reference an attribute of an instance using its selector function.
+  For example, \<^term>\<open>int1 \<sigma>\<close> denotes the value
+  of the \<^term>\<open>int1\<close> attribute
+  of the future instance of the class @{doc_class class_inv1}.
+  Now let's define two instances, one of each class:\<close>
+
+text*[testinv1::class_inv1, int1=4]\<open>lorem ipsum...\<close>
+text*[testinv2::class_inv2, int1=3, int2=1]\<open>lorem ipsum...\<close>
+
+text\<open>
+  The value of each attribute defined for the instances is checked against their classes invariants.
+  As the class @{doc_class class_inv2} is a subsclass of the class @{doc_class class_inv1},
+  it inherits @{doc_class class_inv1} invariants.
+  Hence the \<^term>\<open>int1\<close> invariant is checked when the instance @{docitem testinv2} is defined.\<close>
+
+text\<open>Now assume the following ontology:\<close>
+
+doc_class title =
+  short_title :: "string option" <= "None"
+
+doc_class author =
+  email :: "string" <= "''''"
+
+datatype classification = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
+
+doc_class abstract =
+  keywordlist :: "string list" <= "[]"
+  safety_level :: "classification" <= "SIL3"
+
+doc_class text_section =
+  authored_by :: "author set" <= "{}"
+  level :: "int option" <= "None"
+
+type_synonym notion = string
+
+doc_class introduction = text_section +
+  authored_by :: "author set"  <= "UNIV" 
+  uses :: "notion set"
+  invariant author_finite :: "finite (authored_by \<sigma>)"
+  and force_level :: "the (level \<sigma>) > 1"
+
+doc_class claim = introduction +
+  based_on :: "notion list"
+
+doc_class technical = text_section +
+  formal_results :: "thm list" 
+
+doc_class "definition" = technical +
+  is_formal :: "bool"
+  property  :: "term list" <= "[]" 
+
+datatype kind = expert_opinion | argument | "proof"
+
+doc_class result = technical +
+  evidence :: kind
+  property :: "thm list" <= "[]"
+  invariant has_property :: "evidence \<sigma> = proof \<longleftrightarrow> property \<sigma> \<noteq> []"
+
+doc_class example = technical +
+  referring_to :: "(notion + definition) set" <= "{}"
+
+doc_class conclusion = text_section +
+  establish :: "(claim \<times> result) set"
+  invariant establish_defined :: "\<forall> x. x \<in> Domain (establish \<sigma>)
+                                           \<longrightarrow> (\<exists> y \<in> Range (establish \<sigma>). (x, y) \<in> establish \<sigma>)"
+
+text\<open>Next we define some instances (docitems): \<close>
+
+declare[[invariants_checking_with_tactics = true]]
+
+text*[church::author, email="\<open>church@lambda.org\<close>"]\<open>\<close>
+(*text*[introduction1::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 0"]\<open>\<close>*)
+
+text*[resultProof::result, evidence = "proof", property="[@{thm \<open>HOL.refl\<close>}]"]\<open>\<close>
+text*[resultArgument::result, evidence = "argument"]\<open>\<close>
+
+text\<open>The invariants \<^theory_text>\<open>author_finite\<close> and \<^theory_text>\<open>establish_defined\<close> can not be checked directly
+  and need a little help.
+  We can set the \<open>invariants_checking_with_tactics\<close> theory attribute to help the checking.
+  It will enable a basic tactic, using unfold and auto:\<close>
+
+declare[[invariants_checking_with_tactics = true]]
+
+text*[curry::author, email="\<open>curry@lambda.org\<close>"]\<open>\<close>
+text*[introduction2::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
+text*[introduction3::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
+text*[introduction4::introduction, authored_by = "{@{author \<open>curry\<close>}}", level = "Some 4"]\<open>\<close>
+
+text*[resultProof2::result, evidence = "proof", property="[@{thm \<open>HOL.sym\<close>}]"]\<open>\<close>
+
+text\<open>Then we can evaluate expressions with instances:\<close>
+
+term*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
+value*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
+value*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction4\<close>}\<close>
+
+value*\<open>@{introduction \<open>introduction2\<close>}\<close>
+
+value*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>
+
+term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
+value*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
+
+value*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
+
+declare[[invariants_checking_with_tactics = false]]
+
+end

src/tests/Ontology_Matching_Example.thy

@@ -0,0 +1,52 @@
+chapter\<open>Ontologys Mathing\<close>
+
+theory Ontology_Matching_Example
+  imports "Isabelle_DOF.Isa_DOF"
+begin
+
+text\<open>Using HOL, we can define a mapping between two ontologies.
+  It is called ontology matching or ontology alignment.
+  Here is an example which show how to map two classes.
+  HOL also allows us to map the invariants (ontological rules) of the classes!\<close>
+
+type_synonym UTF8 = string
+
+definition utf8_to_string
+  where "utf8_to_string x = x"
+
+
+doc_class A =
+  first_name :: UTF8
+  last_name :: UTF8
+  age :: nat
+  married_to :: "string option"
+  invariant a :: "age \<sigma> < 18 \<longrightarrow> married_to \<sigma> = None"
+doc_class B =
+  name :: string 
+  adult :: bool
+  is_married :: bool
+  invariant b :: "is_married \<sigma> \<longrightarrow> adult \<sigma>"
+
+text\<open>We define the mapping between the two classes,
+  i.e. how to transform the class @{doc_class A} in to the class @{doc_class B}:\<close>
+
+definition A_to_B_morphism
+  where "A_to_B_morphism X =
+        \<lparr> tag_attribute = A.tag_attribute X
+          , name = utf8_to_string (first_name X) @ '' ''  @ utf8_to_string (last_name X)
+          , adult = (age X \<ge> 18)
+          , is_married = (married_to X \<noteq> None) \<rparr>" 
+
+text\<open>Now we check that the invariant is preserved through the morphism:\<close>
+
+lemma inv_a_preserved :
+  "a_inv X \<Longrightarrow> b_inv (A_to_B_morphism X)"
+  unfolding a_inv_def b_inv_def A_to_B_morphism_def
+  by auto
+
+lemma A_morphism_B_total :
+  "A_to_B_morphism ` ({X::A. a_inv X}) \<subseteq> ({X::B. b_inv X})"
+  using inv_a_preserved
+  by auto
+
+end

src/tests/ROOT

@@ -2,7 +2,10 @@ session "Isabelle_DOF-tests" = "Isabelle_DOF" +
   options [document = false]
   theories
     "AssnsLemmaThmEtc" 
-    "Concept_ExampleInvariant"
+    "Concept_Example_Low_Level_Invariant"
     "Concept_Example"
     "TermAntiquotations"
     "Attributes"
+    "Evaluation"
+    "High_Level_Syntax_Invariants"
+    "Ontology_Matching_Example"

src/tests/TermAntiquotations.thy

@@ -62,6 +62,15 @@ text\<open>Example for a meta-attribute of ODL-type @{typ "typ"} with an appropr
      theorem @{thm "refl"}}\<close>
 text*[xcv2::C, g="@{thm ''HOL.refl''}"]\<open>Lorem ipsum ...\<close>
 
+text\<open>A warning about the usage of the \<open>docitem\<close> TA:
+The \<open>docitem\<close> TA offers a way to check the reference of class instances
+without checking the instances type.
+So one will be able to reference \<open>docitem\<close>s (class instances) and have them checked,
+without the burden of the type checking required otherwise.
+But it may give rise to unwanted behaviors, due to its polymorphic type.
+It must not be used for certification.
+\<close>
+
 text\<open>Major sample: test-item of doc-class \<open>F\<close> with a relational link between class instances, 
      and links to formal Isabelle items like \<open>typ\<close>, \<open>term\<close> and \<open>thm\<close>. \<close>
 text*[xcv4::F, r="[@{thm ''HOL.refl''}, 
@@ -79,8 +88,31 @@ a @{typ "C"}-type is required, but a  @{typ "G"}-type is offered which is legal
 \verb+Isa_DOF+ because of the sub-class relation between those classes: \<close>
 update_instance*[xcv4::F, b+="{(@{docitem ''xcv3''},@{docitem ''xcv5''})}"]
 
-text\<open>And here is the result on term level:\<close>
+text\<open>And here is the results of some ML-term antiquotations:\<close>
 ML\<open> @{docitem_attribute b::xcv4} \<close>
+ML\<open> @{docitem xcv4}              \<close>
+ML\<open> @{trace_attribute aaa}       \<close>
+
+text\<open>Now we might need to reference a class instance in a term command and we would like
+Isabelle to check that this instance is indeed an instance of this class.
+Here, we want to reference the instance @{docitem \<open>xcv4\<close>} previously defined.
+We can use the term* command which extends the classic term command
+and does the appropriate checking.\<close>
+term*\<open>@{F \<open>xcv4\<close>}\<close>
+
+text\<open>We can also reference an attribute of the instance.
+Here we reference the attribute r of the class F which has the type @{typ \<open>thm list\<close>}.\<close>
+term*\<open>r @{F \<open>xcv4\<close>}\<close>
+
+term \<open>@{A \<open>xcv2\<close>}\<close>
+
+text\<open>We declare a new text element. Note that the class name contains an underscore "_".\<close>
+text*[te::text_element]\<open>Lorem ipsum...\<close>
+
+text\<open>Unfortunately due to different lexical conventions for constant symbols and mixfix symbols
+     this term antiquotation has to be denoted like this: @{term\<open>@{text-element \<open>ee\<close>}\<close>}.
+     We need to substitute an hyphen "-" for the underscore "_".\<close>
+term*\<open>@{text-element \<open>te\<close>}\<close>
 
 end