From: Burkhart Wolff <wolff@lri.fr>
Dear Isabelle-Users,
We proudly present Isabelle/DOF, an extension
of the Isabelle’s document generation system by
a general mechanism to annotate typed meta-data
to text, code, and term-elements. The meta-data
Is specified inside Isabelle/HOL theories via so-called
ontologies, which generate an infra-structure for
text and term antiquotations, navigation in PIDE,
and text-generation.
A suite of examples ranging from standard scientific
papers to technical documentations, for example
as used in formal certifications of software.
The main distribution side is
https://zenodo.org/record/4625170#.YswoY-xBxUM <https://zenodo.org/record/4625170#.YswoY-xBxUM> ,
our developper git can be found under:
https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF <https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF>
NEWS:
Ontology ‘scholarly_paper’ with LNCS´style support
(generating for LIPICS-style is possible but requires
some fiddling by hand - UNSUPPORTED FEATURE)
Ontology ‘CENELEC 50128’ to support CENELEC certifications,
a use-case for software-engineering
Integration into the Isabelle-Component-Framework
has been renamed to
dof_mkroot` (and reimplemented in Scala).Enjoy!
Achim Brucker, Idir Ait-Sadoune, Nicolas Méric and Burkhart
Last updated: Jan 04 2025 at 20:18 UTC