Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Use author*.

This commit is contained in:
Achim D. Brucker 2020-11-03 21:50:19 +00:00
parent 1ad81aff35
commit 0b52e5872d
1 changed files with 5 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
examples/scholarly_paper/2020-iFM-CSP/paper.thy
View File

@ -16,26 +16,23 @@ setup \<open> DOF_lib.define_shortcut \<^binding>\<open>csp\<close> "CSP
title*[tit::title]\<open>Philosophers may Dine - Definitively!\<close> title*[tit::title]\<open>Philosophers may Dine - Definitively!\<close>
(* new crashing variant 1:
author*[safouan, email="''safouan.taha@lri.fr''",affiliation="\<open>LRI, CentraleSupelec\<close>"] author*[safouan, email="''safouan.taha@lri.fr''",affiliation="\<open>LRI, CentraleSupelec\<close>"]
\<open>Safouan Taha\<close> \<open>Safouan Taha\<close>
*) (*
author*[safouann::author, email="''safouan.taha@lri.fr''",affiliation="\<open>LRI, CentraleSupelec\<close>"]
(* new crashing variant 2:
author*[safouan::author, email="''safouan.taha@lri.fr''",affiliation="\<open>LRI, CentraleSupelec\<close>"]
\<open>Safouan Taha\<close> \<open>Safouan Taha\<close>
*) text*[safouannn::author, email="''safouan.taha@lri.fr''",affiliation="\<open>LRI, CentraleSupelec\<close>"]
text*[safouan::author, email="''safouan.taha@lri.fr''",affiliation="\<open>LRI, CentraleSupelec\<close>"]
\<open>Safouan Taha\<close> \<open>Safouan Taha\<close>
*)
text*[bu::author, email= "''wolff@lri.fr''",affiliation = "\<open>LRI, Université Paris-Saclay\<close>"] text*[bu::author, email= "''wolff@lri.fr''",affiliation = "\<open>LRI, Université Paris-Saclay\<close>"]
\<open>Burkhart Wolff\<close> \<open>Burkhart Wolff\<close>
text*[lina::author,email="''lina.ye@lri.fr''",affiliation="\<open>LRI, Inria, LSV, CentraleSupelec\<close>"] text*[lina::author,email="''lina.ye@lri.fr''",affiliation="\<open>LRI, Inria, LSV, CentraleSupelec\<close>"]
\<open>Lina Ye\<close> \<open>Lina Ye\<close>
text*[abs::abstract, keywordlist="[\<open>Shallow Embedding\<close>,\<open>Process-Algebra\<close>, abstract*[abs, keywordlist="[\<open>Shallow Embedding\<close>,\<open>Process-Algebra\<close>,
\<open>Concurrency\<close>,\<open>Computational Models\<close>]"] \<open>Concurrency\<close>,\<open>Computational Models\<close>]"]
\<open> The theory of Communicating Sequential Processes going back to Hoare and Roscoe is \<open> 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. still today one of the reference theories for concurrent specification and computing.