No Description
Burkhart Wolff 90f6c2d4ab - New checks for reject sets 10 hours ago
AFP-contribs for documentation 2 weeks ago
document-generator Require subfloat (required for side_by_side_figure). 1 week ago
examples - New checks for reject sets - basic infrastructure for class invariants 10 hours ago
old Kleinigkeiten um MathExam. 4 months ago
ontologies Introduced Syntax accept / reject. added some semantic for it (incomplete) some elements on myCommentedIsabelle 1 week ago
patches comment inside meta_args problem solved. 1 month ago
test small follower bug. 2 months ago
.gitignore Added: simple test setup. 8 months ago
Assert.thy Kind of current status. 9 months ago
AssertLong.thy Kind of current status. 9 months ago
CITATION Initial commit. 5 months ago
Isa_COL.thy implemented reject alphabets. (untested) slight corrections in MyCommentedIsabelle (MCI) 23 hours ago
Isa_DOF.thy - New checks for reject sets - basic infrastructure for class invariants 10 hours ago
LICENSE Moved license information to top-level directory. 5 months ago Updated README with basic installation instructions. 5 months ago
ROOT New Config for 2017 including AFP contributions for Regular-Sets and Regular Automata. Added a thin layer interfacing these two. Slight textual improvements of examples (updates to more recent notations). 3 weeks ago
ROOTS Updated ROOT(s) setup to include AFP entries ... 2 weeks ago
RegExp.thy - Improved automata-management - automata transformation integrated - control option strict_checking added - rudimentary tests in IsaDofApplications and Monitor_Example 2 weeks ago
RegExpChecker.sml New Config With AFP components and a thin interface for monitor-checking. 2 weeks ago
RegExpInterface.thy - New checks for reject sets - basic infrastructure for class invariants 10 hours ago
TODO Updated todo items. 5 months ago
install Added version check. 1 week 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.


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 argument to the install script:

foo@bar:~$ ./install /usr/local/Isabelle2016-1/bin/isabelle

The DOF-plugin will be installed in the Isabelle user directory (the exact location depends on the Isabelle version).


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_50126
       * 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, Springer-Verlag, 2018.