We are proud to announce the first public release of Isabelle/DOF. Isabelle/DOF is a Document Ontology Framework (DOF) allowing annotating text elements in formal developments with structured, typed meta-information. Developers can define this meta-information according to their needs, e.g., to enable semantic queries (in the sense of semantic web), tool interaction, or document generation.

Currently, Isabelle/DOF focuses on the generation of documents with formal and semi-formal or informal content. While Isabelle/DOF is developed on top of Isabelle/HOL, its users are not necessarily Isabelle users: Isabelle/DOF aims at authors of any type of documents involving formal content or formal structure. Possible application areas are, e.g., mathematical papers, or documents with certification processes.

Isabelle/DOF can be downloaded from its website: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/ Alternatively, a Docker image is available that allows to directly start Isabelle/DOF (this requires a host operating system with an X-Sever):

docker run -ti --rm -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-unix \
           logicalhacking/isabelle_dof-1.0.0_isabelle2019 isabelle jedit

As the Isabelle/DOF installation requires applying a small patch to Isabelle itself, the Docker image is helpful for users that want to avoid modifying Isabelle itself.

The Isabelle/DOF distribution contains the Isabelle/DOF: User and Implementation Manual and the system is also described in [1] and [2]. The manual and [2] are written using Isabelle/DOF.

Supplementary Material

• Isabelle/DOF Website: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/
• Isabelle_DOF-1.0.0_Isabelle2019.pdf
• Isabelle_DOF-1.0.0_Isabelle2019.tar.xz
• Isabelle_DOF-1.0.0_Isabelle2019.tar.xz.asc

References