diff --git a/CITATION b/CITATION new file mode 100644 index 00000000..5fb01eba --- /dev/null +++ b/CITATION @@ -0,0 +1,29 @@ +To cite Isabelle/DOF in publications, please use + + + Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart + Wolff. Using The Isabelle Ontology Framework: Linking the Formal + with the Informal. In Conference on Intelligent Computer Mathematics + (CICM). Lecture Notes in Computer Science, Springer-Verlag, 2018. + +A BibTeX entry for LaTeX users is + +@InCollection{ brucker.ea:isabelle-ontologies:2018, + url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelle-ontologies-2018}, + keywords = {Isabelle/Isar, HOL, Ontologies}, + location = {Hagenberg, Austria}, + author = {Achim D. Brucker and Idir Ait-Sadoune and Paolo Crisafulli + and Burkhart Wolff}, + booktitle = {Conference on Intelligent Computer Mathematics (CICM)}, + language = {USenglish}, + publisher = {Springer-Verlag}, + address = {Heidelberg}, + series = {Lecture Notes in Computer Science}, + title = {Using The Isabelle Ontology Framework: Linking the Formal + with the Informal}, + classification= {conference}, + areas = {formal methods, software engineering}, + public = {yes}, + year = {2018}, + pdf = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf} +} diff --git a/document-generator/latex/DOF-core.sty b/document-generator/latex/DOF-core.sty index dd481353..e4ec8f80 100644 --- a/document-generator/latex/DOF-core.sty +++ b/document-generator/latex/DOF-core.sty @@ -88,3 +88,6 @@ #1 \end{isamarkuptext}% } + +\newkeycommand\isaDofOpenMonitor[label=,type=]{} +\newkeycommand\isaDofCloseMonitor[label=,type=]{} diff --git a/document-generator/latex/DOF-mathex.sty b/document-generator/latex/DOF-mathex.sty index 9800703b..fea7247a 100644 --- a/document-generator/latex/DOF-mathex.sty +++ b/document-generator/latex/DOF-mathex.sty @@ -89,3 +89,7 @@ \newkeycommand\isaDofSubsubsectionMathExam[label=,type=,content=,global_grade=][1]{% #1 } + + +\newkeycommand\isaDofOpenMonitorMathExam[label=,type=]{} +\newkeycommand\isaDofCloseMonitorMathExam[label=,type=]{} diff --git a/examples/math_exam/MathExam/MathExam.thy b/examples/math_exam/MathExam/MathExam.thy index d517f09d..00a51dfc 100644 --- a/examples/math_exam/MathExam/MathExam.thy +++ b/examples/math_exam/MathExam/MathExam.thy @@ -3,8 +3,8 @@ theory MathExam imports "../../../ontologies/mathex_onto" Real begin -open_monitor*[exam::MathExam] (*>*) +open_monitor*[exam::MathExam] section*[idir::Author, affiliation="''CentraleSupelec''", email="''idir.aitsadoune@centralesupelec.fr''"] @@ -71,7 +71,5 @@ Prove that @{term "n*(n+5) + 2*(n+3) "} is always the product of two numbers with a difference of 5. *} -(*<*) -close_monitor*[exam] -(*>*) +close_monitor*[exam::MathExam] end