Activated MathExam.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
This commit is contained in:
parent
7f8ea1c115
commit
e6cea1156c
|
@ -1,7 +1,7 @@
|
||||||
(*<*)
|
(*<*)
|
||||||
theory MathExam
|
theory MathExam
|
||||||
imports "Isabelle_DOF.mathex_onto"
|
imports "Isabelle_DOF.mathex_onto"
|
||||||
Real
|
HOL.Real
|
||||||
begin
|
begin
|
||||||
(*>*)
|
(*>*)
|
||||||
open_monitor*[exam::MathExam]
|
open_monitor*[exam::MathExam]
|
||||||
|
@ -22,18 +22,9 @@ text*[idir::Author, affiliation="''CentraleSupelec''",
|
||||||
{*Idir AIT SADOUNE*}
|
{*Idir AIT SADOUNE*}
|
||||||
|
|
||||||
|
|
||||||
(* should be in DOF-core
|
|
||||||
|
|
||||||
* causes crash on the LaTeX side:
|
|
||||||
( FP-DIV )
|
|
||||||
*** ! Undefined control sequence.
|
|
||||||
*** <argument> ...ative_width}}{100} \includegraphics
|
|
||||||
*** [width=\scale \textwidth ]...
|
|
||||||
*** l.44 {A Polynome.}
|
|
||||||
*)
|
|
||||||
figure*[figure::figure, spawn_columns=False,
|
figure*[figure::figure, spawn_columns=False,
|
||||||
relative_width="80",
|
relative_width="80",
|
||||||
src="''figures/Polynomialdeg5.png''"]
|
src="''figures/Polynomialdeg5''"]
|
||||||
\<open>A Polynome.\<close>
|
\<open>A Polynome.\<close>
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -0,0 +1 @@
|
||||||
|
MathExam
|
Loading…
Reference in New Issue