Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF

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}
+}

document-generator/latex/DOF-core.sty

@@ -88,3 +88,6 @@
       #1
   \end{isamarkuptext}%
 }
+
+\newkeycommand\isaDofOpenMonitor[label=,type=]{}
+\newkeycommand\isaDofCloseMonitor[label=,type=]{}

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=]{}

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