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

no message

This commit is contained in:
Idir AIT SADOUNE 2018-04-30 13:13:53 +02:00
parent 49e3ec81f7
commit 86cce02f7a
2 changed files with 28 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
examples/simple/MathExam.thy
View File

@ -4,30 +4,39 @@ begin
open_monitor*[exam::MathExam]
text*[idir::Author, affiliation="''CentraleSupelec''",
email="''idir.aitsadoune@centralesupelec.fr''"]
text*[idir::Author, affiliation="''CentraleSupelec''", email="''idir.aitsadoune@centralesupelec.fr''"]
{*Idir AIT SADOUNE*}
text*[header::Header,examSubject= "algebra", examTitle="''Exam number 1''"]
{* Please follow directions carefully and show all your work.*}
section*[exo1 :: Exercise, Exercise.content="[q1::Question,q2,q3]", mark="15::int"]{* Exercise 1.*}
text*[q1::Question, level="twoStars", Question.mark="5::int"]
{*
Give an example of each of the following :
text*[header::Header,examSubject= "algebra", examTitle="''Exam number 1''", date="''02-05-2018''",timeAllowed="90::int"]
{*
\begin{itemize}
\item - a rational number which is not integer.
\item - a real number which is not rational.
\item Use black ink or black ball-point pen.
\item Draw diagrams in pencil.
\item Answer all questions in the spaces provided.
\end{itemize}
*}
text*[q2::Question, level="oneStar", Question.mark="5::int"]
{*
Write in interval notation : @{term "-3 < x"} and @{term "x < 5"}
section*[exo1 :: Exercise, Exercise.content="[q1::Question,q2::Question]"]
{*
Here are the first four lines of a number pattern.
\begin{itemize}
\item Line 1 : @{term "1*6 + 2*4 = 2*7"}
\item Line 2 : @{term "2*7 + 2*5 = 3*8"}
\item Line 3 : @{term "3*8 + 2*6 = 4*9"}
\item Line 4 : @{term "4*9 + 2*7 = 5*10"}
\end{itemize}
*}
text*[q1::Question, level="oneStar", Question.mark="1::int", type="formal"]
{*
Complete Line 10 : @{term "10*x + 2*y = 11*16"}
*}
text*[q2::Question, level="threeStars", Question.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.
*}
text*[q3::Question, level="oneStar", Question.mark="5::int"]
{* True or false : @{term "0/8 = 0"} *}
close_monitor*[exam]

4
ontologies/mathex_onto.thy
View File

@ -31,6 +31,8 @@ datatype Grade =
doc_class Header =
examTitle :: string
examSubject :: Subject
date :: string
timeAllowed :: int -- minutes
datatype ContentClass =
examiner -- \<open>the 'author' of the exam\<close>
@ -52,7 +54,7 @@ doc_class Question = Exam_item +
doc_class Exercise = Exam_item +
content :: "(Question) list"
concerns :: "ContentClass set" <= "{examiner,validator,student}"
mark :: int
text{* In many institutions, it makes sense to have a rigorous process of validation
for exam subjects : is the initial question correct ? Is a proof in the sense of the