Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for both conventional typesetting as well as formal development.
You cannot select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
Go to file
Achim D. Brucker eac94f2a01 Merge branch 'Isabelle_dev' 7 months ago
.woodpecker Merge branch 'Isabelle_dev' 7 months ago
etc Update to Isabelle 2022. 7 months ago
examples Merge branch 'main' into Isabelle_dev 7 months ago
src Update to Isabelle 2022. 7 months ago
.gitattributes Initial commit. 11 months ago
.gitignore Ignore Isabelle/JEdit tmp files. 1 year ago Update to Isabelle 2022. 7 months ago
CITATION Fixed file attributes. 1 year ago
LICENSE Fixed file attributes. 1 year ago Linting. 7 months ago
ROOTS Fixed file attributes. 1 year ago
install-afp Declared installation script as deprecated. 7 months 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 and formal development. The manual for Isabelle/DOF 1.3.0/Isabelle2021-1 is available online.


Isabelle/DOF has three major prerequisites:


Isabelle/DOF is provided as an Isabelle component. After installing the prerequisites, change into the directory containing Isabelle/DOF (this should be the directory containing this file) and execute (if you executed this command already during the installation of the prerequisites, you can skip it now):

foo@bar:~$ isabelle components -u `pwd`

The final step for the installation is:

foo@bar:~$ isabelle build -D .

This will compile Isabelle/DOF and run the example suite.


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

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. For example,

foo@bar:~$ isabelle dof_mkroot -o scholarly_paper -t scrartcl

creates a setup using the scholarly_paper ontology and the article class from the KOMA-Script bundle.

The help (option -h) show a list of all supported ontologies and document templates:

foo@bar:~$ isabelle dof_mkroot -h
Usage: isabelle dof_mkroot [OPTIONS] [DIRECTORY]

  Options are:
    -I           init Mercurial repository and add generated files
    -n NAME      alternative session name (default: directory base name)
    -o ONTOLOGY  ontology (default: scholarly_paper)
    -t TEMPLATE  tempalte (default: scrartcl)

  Prepare session root directory (default: current directory).


For releases, signed archives including a PDF version of the Isabelle/DOF manual are available:

Older Releases


Main contacts:


  • Idir Ait-Sadoune
  • Paolo Crisafulli
  • Chantal Keller
  • Nicolas Méric


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

SPDX-License-Identifier: BSD-2-Clause


Upstream Repository

The upstream git repository, i.e., the single source of truth, for this project is hosted at