From c991e693dc2bccd11c93ce2a48b1c71e8c1d43fd Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Wed, 4 Nov 2020 02:52:55 +0100 Subject: [PATCH] tested and enforced new author* and abstract* macros. --- .../IsaDofApplications.thy | 61 +++++++++---------- .../scholarly_paper/2020-iFM-CSP/paper.thy | 23 +++---- 2 files changed, 37 insertions(+), 47 deletions(-) diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy index a37c2ac..173f3b1 100755 --- a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy +++ b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy @@ -22,39 +22,38 @@ declare[[strict_monitor_checking=false]] title*[tit::title]\Using the Isabelle Ontology Framework\ subtitle*[stit::subtitle]\Linking the Formal with the Informal\ -text*[adb:: author, - email="''a.brucker@sheffield.ac.uk''", - orcid="''0000-0002-6355-1200''", - affiliation="''The University of Sheffield, Sheffield, UK''"]\Achim D. Brucker\ -text*[idir::author, - email = "''idir.aitsadoune@centralesupelec.fr''", - affiliation = "''CentraleSupelec, Paris, France''"]\Idir Ait-Sadoune\ -text*[paolo::author, - email = "''paolo.crisafulli@irt-systemx.fr''", - affiliation= "''IRT-SystemX, Paris, France''"]\Paolo Crisafulli\ -text*[bu::author, - email = "\wolff@lri.fr\", - affiliation = "\Université Paris-Saclay, Paris, France\"]\Burkhart Wolff\ +author*[adb, + email ="''a.brucker@sheffield.ac.uk''", + orcid ="''0000-0002-6355-1200''", + affiliation ="''The University of Sheffield, Sheffield, UK''"]\Achim D. Brucker\ +author*[idir, + email = "''idir.aitsadoune@centralesupelec.fr''", + affiliation = "''CentraleSupelec, Paris, France''"]\Idir Ait-Sadoune\ +author*[paolo, + email = "''paolo.crisafulli@irt-systemx.fr''", + affiliation = "''IRT-SystemX, Paris, France''"]\Paolo Crisafulli\ +author*[bu, + email = "\wolff@lri.fr\", + affiliation = "\Université Paris-Saclay, Paris, France\"]\Burkhart Wolff\ -text*[abs::abstract, - keywordlist="[''Ontology'',''Ontological Modeling'',''Isabelle/DOF'']"]\ -While Isabelle is mostly known as part of Isabelle/HOL (an interactive -theorem prover), it actually provides a framework for developing a wide -spectrum of applications. A particular strength -of the Isabelle framework is the combination of text editing, formal verification, -and code generation. - -Up to now, Isabelle's document preparation system lacks a mechanism -for ensuring the structure of different document types (as, e.g., -required in certification processes) in general and, in particular, -mechanism for linking informal and formal parts of a document. - -In this paper, we present \isadof, a novel Document Ontology Framework -on top of Isabelle. \isadof allows for conventional typesetting -\<^emph>\as well\ as formal development. We show how to model document - ontologies inside \isadof, how to use the resulting meta-information -for enforcing a certain document structure, and discuss ontology-specific IDE support. +abstract*[abs::abstract, keywordlist="[''Ontology'',''Ontological Modeling'',''Isabelle/DOF'']"]\ + While Isabelle is mostly known as part of Isabelle/HOL (an interactive + theorem prover), it actually provides a framework for developing a wide + spectrum of applications. A particular strength + of the Isabelle framework is the combination of text editing, formal verification, + and code generation. + + Up to now, Isabelle's document preparation system lacks a mechanism + for ensuring the structure of different document types (as, e.g., + required in certification processes) in general and, in particular, + mechanism for linking informal and formal parts of a document. + + In this paper, we present \isadof, a novel Document Ontology Framework + on top of Isabelle. \isadof allows for conventional typesetting + \<^emph>\as well\ as formal development. We show how to model document + ontologies inside \isadof, how to use the resulting meta-information + for enforcing a certain document structure, and discuss ontology-specific IDE support. \ section*[intro::introduction]\ Introduction \ diff --git a/examples/scholarly_paper/2020-iFM-CSP/paper.thy b/examples/scholarly_paper/2020-iFM-CSP/paper.thy index 52198b0..097d797 100644 --- a/examples/scholarly_paper/2020-iFM-CSP/paper.thy +++ b/examples/scholarly_paper/2020-iFM-CSP/paper.thy @@ -18,27 +18,18 @@ title*[tit::title]\Philosophers may Dine - Definitively!\ author*[safouan, email="''safouan.taha@lri.fr''",affiliation="\LRI, CentraleSupelec\"] \Safouan Taha\ - -(* -author*[safouann::author, email="''safouan.taha@lri.fr''",affiliation="\LRI, CentraleSupelec\"] - \Safouan Taha\ - -text*[safouannn::author, email="''safouan.taha@lri.fr''",affiliation="\LRI, CentraleSupelec\"] - \Safouan Taha\ -*) - -text*[bu::author, email= "''wolff@lri.fr''",affiliation = "\LRI, Université Paris-Saclay\"] +author*[bu, email= "''wolff@lri.fr''",affiliation = "\LRI, Université Paris-Saclay\"] \Burkhart Wolff\ -text*[lina::author,email="''lina.ye@lri.fr''",affiliation="\LRI, Inria, LSV, CentraleSupelec\"] +author*[lina,email="''lina.ye@lri.fr''",affiliation="\LRI, Inria, LSV, CentraleSupelec\"] \Lina Ye\ abstract*[abs, keywordlist="[\Shallow Embedding\,\Process-Algebra\, \Concurrency\,\Computational Models\]"] -\ The theory of Communicating Sequential Processes going back to Hoare and Roscoe is - still today one of the reference theories for concurrent specification and computing. - In 1997, a first formalization in \<^isabelle> of the denotational semantics of the - Failure/Divergence Model of \<^csp> was undertaken; in particular, this model can cope with infinite - alphabets, in contrast to model-checking approaches limited to finite ones. +\ The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today + one of the reference theories for concurrent specification and computing. In 1997, a first + formalization in \<^isabelle> of the denotational semantics of the Failure/Divergence Model of + \<^csp> was undertaken; in particular, this model can cope with infinite alphabets, in contrast + to model-checking approaches limited to finite ones. In this paper, we extend this theory to a significant degree by taking advantage of more powerful automation of modern Isabelle version, which came even closer to recent developments in the semantic foundation of \<^csp>.