nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

LaTeX support for monitors.

This commit is contained in:
Achim D. Brucker 2018-06-12 08:45:37 +01:00
parent 899f74f2f0
commit bab84243d2
3 changed files with 9 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
document-generator/latex/DOF-core.sty
View File

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

4
document-generator/latex/DOF-mathex.sty
View File

@ -89,3 +89,7 @@
\newkeycommand\isaDofSubsubsectionMathExam[label=,type=,content=,global_grade=][1]{%
#1
}
\newkeycommand\isaDofOpenMonitorMathExam[label=,type=]{}
\newkeycommand\isaDofCloseMonitorMathExam[label=,type=]{}

6
examples/math_exam/MathExam/MathExam.thy
View File

@ -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''"]
@ -70,7 +70,5 @@ text*[q2::Task, level="threeStars", mark="3::int", type="formal"]
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