diff --git a/examples/ROOTS b/examples/ROOTS index 93b168d..1adbab0 100755 --- a/examples/ROOTS +++ b/examples/ROOTS @@ -1,3 +1,4 @@ scholarly_paper +technical_report math_exam CENELEC_50128 diff --git a/examples/scholarly_paper/2020-iFM-CSP/paper.thy b/examples/scholarly_paper/2020-iFM-CSP/paper.thy index 34bf1f0..b727d04 100644 --- a/examples/scholarly_paper/2020-iFM-CSP/paper.thy +++ b/examples/scholarly_paper/2020-iFM-CSP/paper.thy @@ -16,12 +16,9 @@ setup \ DOF_lib.define_shortcut \<^binding>\csp\ "CSP title*[tit::title]\Philosophers may Dine - Definitively!\ -author*[safouan, email="''safouan.taha@lri.fr''",affiliation="\LRI, CentraleSupelec\"] - \Safouan Taha\ -author*[bu, email= "''wolff@lri.fr''",affiliation = "\LRI, Université Paris-Saclay\"] - \Burkhart Wolff\ -author*[lina,email="''lina.ye@lri.fr''",affiliation="\LRI, Inria, LSV, CentraleSupelec\"] - \Lina Ye\ +author*[safouan,email="\safouan.taha@lri.fr\",affiliation="\LRI, CentraleSupelec\"]\Safouan Taha\ +author*[bu,email= "\wolff@lri.fr\",affiliation = "\LRI, Université Paris-Saclay\"]\Burkhart Wolff\ +author*[lina,email="\lina.ye@lri.fr\",affiliation="\LRI, Inria, LSV, CentraleSupelec\"]\Lina Ye\ abstract*[abs, keywordlist="[\Shallow Embedding\,\Process-Algebra\, \Concurrency\,\Computational Models\]"] diff --git a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy index 193b76e..18732d6 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy @@ -100,47 +100,46 @@ open_monitor*[this::report] (*>*) -title*[title::title]\Isabelle/DOF\ +title*[title::title] \Isabelle/DOF\ subtitle*[subtitle::subtitle]\User and Implementation Manual\ -text*[adb:: author, - email="\a.brucker@exeter.ac.uk\", - orcid="\0000-0002-6355-1200\", - http_site="\https://www.brucker.ch/\", - affiliation="\University of Exeter, Exeter, UK\"]\Achim D. Brucker\ -text*[bu::author, - email = "\wolff@lri.fr\", - affiliation = "\Université Paris-Saclay, LRI, Paris, France\"]\Burkhart Wolff\ +author*[ adb, + email ="\a.brucker@exeter.ac.uk\", + orcid ="\0000-0002-6355-1200\", + http_site ="\https://www.brucker.ch/\", + affiliation ="\University of Exeter, Exeter, UK\"]\Achim D. Brucker\ +author*[ bu, + email = "\wolff@lri.fr\", + affiliation = "\Université Paris-Saclay, LRI, Paris, France\"]\Burkhart Wolff\ -text*[abs::abstract, - keywordlist="[''Ontology'', ''Ontological Modeling'', ''Document Management'', - ''Formal Document Development'', ''Document Authoring'', ''Isabelle/DOF'']"] -\ \<^isadof> provides an implementation of \<^dof> on top of Isabelle/HOL. - \<^dof> itself is a novel framework for \<^emph>\defining\ ontologies - and \<^emph>\enforcing\ them during document development and document - evolution. \<^isadof> targets use-cases such as mathematical texts referring - to a theory development or technical reports requiring a particular structure. - A major application of \<^dof> is the integrated development of - formal certification documents (\<^eg>, for Common Criteria or CENELEC - 50128) that require consistency across both formal and informal - arguments. +abstract*[abs, keywordlist="[\Ontology\, \Ontological Modeling\, \Document Management\, + \Formal Document Development\,\Document Authoring\,\Isabelle/DOF\]"] +\ \<^isadof> provides an implementation of \<^dof> on top of Isabelle/HOL. + \<^dof> itself is a novel framework for \<^emph>\defining\ ontologies + and \<^emph>\enforcing\ them during document development and document + evolution. \<^isadof> targets use-cases such as mathematical texts referring + to a theory development or technical reports requiring a particular structure. + A major application of \<^dof> is the integrated development of + formal certification documents (\<^eg>, for Common Criteria or CENELEC + 50128) that require consistency across both formal and informal + arguments. - \<^isadof> is integrated into Isabelle's IDE, which - allows for smooth ontology development as well as immediate - ontological feedback during the editing of a document. - Its checking facilities leverage the collaborative - development of documents required to be consistent with an - underlying ontological structure. + \<^isadof> is integrated into Isabelle's IDE, which + allows for smooth ontology development as well as immediate + ontological feedback during the editing of a document. + Its checking facilities leverage the collaborative + development of documents required to be consistent with an + underlying ontological structure. + + In this user-manual, we give an in-depth presentation of the design + concepts of \<^dof>'s Ontology Definition Language (ODL) and describe + comprehensively its major commands. Many examples show typical best-practice + applications of the system. - In this user-manual, we give an in-depth presentation of the design - concepts of \<^dof>'s Ontology Definition Language (ODL) and describe - comprehensively its major commands. Many examples show typical best-practice - applications of the system. - - It is an unique feature of \<^isadof> that ontologies may be used to control - the link between formal and informal content in documents in a machine - checked way. These links can connect both text elements as well as formal - modelling elements such as terms, definitions, code and logical formulas, - alltogether *\integrated\ in a state-of-the-art interactive theorem prover. + It is an unique feature of \<^isadof> that ontologies may be used to control + the link between formal and informal content in documents in a machine + checked way. These links can connect both text elements as well as formal + modelling elements such as terms, definitions, code and logical formulas, + alltogether *\integrated\ in a state-of-the-art interactive theorem prover. \ (*<*) diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/header_CSP_source.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/header_CSP_source.png old mode 100755 new mode 100644 index 598cd91..27975ff Binary files a/examples/technical_report/Isabelle_DOF-Manual/document/figures/header_CSP_source.png and b/examples/technical_report/Isabelle_DOF-Manual/document/figures/header_CSP_source.png differ