No Description
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
Burkhart Wolff b035996d36 petitesse 1 day ago
.ci Fixed name of docker image for CI. 3 months ago
document-generator Dangling references and undefined citations are now breaking the document build. 1 week ago
examples Excluded example of dangling reference from LaTex generation. 1 week ago
ontologies petitesse 1 day ago
patches comment inside meta_args problem solved. 6 months ago
test Renamed CENELEC_50126 to CENELEC_50128 to match actual standard. 2 months ago
.gitattributes Avoid line ending conversions for shell scripts, 4 months ago
.gitignore Ignore local afp installation directory (.afp). 3 months ago
Assert.thy Worked on assert*. 4 months ago
AssertLong.thy Kind of current status. 1 year ago
CITATION Updated bibliographic information. 3 months ago
Isa_COL.thy Small things at CENELEC arising from FM paper. text_elem according to common discussopn with Achim. 5 days ago
Isa_DOF.thy Merge branch 'master' of 2 days ago
LICENSE Moved license information to top-level directory. 10 months ago Changed user interface of the installation script: supports now long and short options and allows one to skipt the lengthy patch and afp installation check. 2 weeks ago
ROOT Renamed CENELEC_50126 to CENELEC_50128 to match actual standard. 2 months ago
ROOTS Removed local AFP entries. 3 months ago
RegExp.thy - Improved automata-management 5 months ago
RegExpChecker.sml New Config With AFP components and a thin interface for monitor-checking. 5 months ago
RegExpInterface.thy - New checks for reject sets 5 months ago
install Changed user interface of the installation script: supports now long and short options and allows one to skipt the lengthy patch and afp installation check. 2 weeks ago

Isabelle/DOF: Document Preparation Setup

Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for both conventional typesetting as well as formal development.


Isabelle/DOF requires Isabelle 2017. Please download the Isabelle 2017 distribution for your operating system from the Isabelle website.


Quick Installation Guide

In most case, the DOF-plugin can be installed as follows:

foo@bar:~$ ./install

If a specific Isabelle version should be used (i.e., not the default one), the full path to the isabelle command needs to be passed as using the -i command line argument of the install script:

foo@bar:~$ ./install -i /usr/local/Isabelle2017/bin/isabelle

For further command line options of the installer, please use the built-in help:

foo@bar:~$ ./install -h

What The Installer Actually Does

The installer will

  • apply a patch to Isabelle that is necessary to use Isabelle/DOF. If this patch installations fails, you need to manually replace the file Isabelle2017/src/Pure/Thy/thy_output.ML in the Isabelle distribution with the file patches/thy_output.ML from the
    Isabelle/DOF distribution:
    console cp patches/thy_output.ML `isabelle getenv -b ISABELLE_HOME`/src/Pure/Thy/
  • install required entries from the AFP. If this installations fails, you need to manually install the AFP for Isabelle 2017 as follows: Download the AFP for Isabelle 2017 and follow the instructions for installing the AFP as Isabelle component. If you have extracted the AFP archive into the directory to /home/myself/afp, you should run the following command to make the AFP session ROOTS available to Isabelle: console echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2017/ROOTS
  • install the Isabelle/DOF-plugin into the Isabelle user directory (the exact location depends on the Isabelle version).
  • check that the AFP has been installed successfully.


Opening an Example

If you want to work with or extend one of the examples, e.g., you can open it similar to any standard Isabelle theory:

isabelle jedit -d . -l Isabelle_DOF examples/scholarly_paper/2018_cicm/IsaDofApplications.thy

This will open an example of a scientific paper using the pre-compiled session Isabelle_DOF, i.e., you will not be able to edit the ontology definitions. If you want to edit the ontology definition, just open the theory file with the default HOL session:

isabelle jedit -d . -l HOL examples/scholarly_paper/2018_cicm/IsaDofApplications.thy

While this gives you more flexibility, it might “clutter” your editing experience, as a lot of internal theories are loaded into Isabelle’s editor.

Creating a New Project

The DOF-plugin provides an alternative to Isabelle’s mkroot command. Isabelle projects that use DOF need to be created using

foo@bar:~$ isabelle DOF_mkroot -d 

The DOF_mkroot command takes the same parameter as the standard mkroot command of Isabelle. Thereafter, the normal Isabelle command for building documents can be used.

Using the -o option, different ontology setups can be selected and using the -t option, different LaTeX setups can be selected (use -h to obtain a list of all installed setups):

foo@bar:~$ isabelle DOF_mkroot -h

Usage: isabelle DOF_mkroot [OPTIONS] [DIR]

  Options are:
    -h           print this help text and exit
    -d           enable document preparation
    -n NAME      alternative session name (default: DIR base name)
    -o ONTOLOGY  (default: core)
       Available ontologies:
       * cenelec_50128
       * core
       * mathex
       * scholarly_paper
       Available document templates:
       * lncs
       * scrreprt

  Prepare session root DIR (default: current directory).

For example,

foo@bar:~$ isabelle DOF_mkroot -d -o scholarly_paper -t lncs

creates a setup using the scholarly_paper ontology and Springer’s LNCS LaTeX class as document class. Note that the generated setup does not include the actual llncs.cls file. This is due to license restrictions. You need to obtain the file from Springer’s website and either copy it in you texmf directory or the root folder. In the latter case, you also need to add it in the ROOT file as dependency.


Main contacts:


  • Idir Ait-Sadoune
  • Paolo Crisafulli
  • Chantal Keller


This project is licensed under a 2-clause BSD license.

SPDX-License-Identifier: BSD-2-Clause


  • Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart Wolff. Using The Isabelle Ontology Framework: Linking the Formal with the Informal. In Conference on Intelligent Computer Mathematics (CICM). Lecture Notes in Computer Science (11006), Springer-Verlag, 2018.