diff --git a/examples/simple/MathExam.thy b/examples/simple/MathExam.thy index 03d7e14..d80493a 100644 --- a/examples/simple/MathExam.thy +++ b/examples/simple/MathExam.thy @@ -4,10 +4,12 @@ begin open_monitor*[exam::MathExam] -text*[idir::Author, affiliation="''CentraleSupelec''", email="''idir.aitsadoune@centralesupelec.fr''"] +section*[idir::Author, affiliation="''CentraleSupelec''", + email="''idir.aitsadoune@centralesupelec.fr''"] {*Idir AIT SADOUNE*} -text*[header::Header,examSubject= "algebra", examTitle="''Exam number 1''", date="''02-05-2018''",timeAllowed="90::int"] +subsection*[header::Header,examSubject= "algebra", examTitle="''Exam number 1''", + date="''02-05-2018''", timeAllowed="90::int"] {* \begin{itemize} \item Use black ink or black ball-point pen. @@ -16,7 +18,7 @@ text*[header::Header,examSubject= "algebra", examTitle="''Exam number 1''", dat \end{itemize} *} -section*[exo1 :: Exercise, Exercise.content="[q1::Question,q2::Question]"] +subsubsection*[exo1 :: Exercise, Exercise.content="[q1::Question,q2::Question]"] {* Here are the first four lines of a number pattern. \begin{itemize} diff --git a/ontologies/mathex_onto.thy b/ontologies/mathex_onto.thy index 7088970..2266bca 100644 --- a/ontologies/mathex_onto.thy +++ b/ontologies/mathex_onto.thy @@ -42,11 +42,11 @@ datatype ContentClass = doc_class Exam_item = concerns :: "ContentClass set" -datatype SubQuestion = Item string +type_synonym SubQuestion = string -doc_class Answer_Formal = Exam_item + - step_label :: string - "term" :: "string" +doc_class Answer_Formal_Step = Exam_item + + justification :: string + "term" :: "string" doc_class Answer_YesNo = Exam_item + step_label :: string @@ -55,16 +55,16 @@ doc_class Answer_YesNo = Exam_item + datatype Question_Type = formal | informal | mixed -doc_class Question = Exam_item + +doc_class Task = Exam_item + level :: Level type :: Question_Type - subitems :: "(SubQuestion * (Answer_Formal + Answer_YesNo)list) list" + subitems :: "(SubQuestion * (Answer_Formal_Step list + Answer_YesNo)list) list" concerns :: "ContentClass set" <= "{examiner,validator,student}" mark :: int doc_class Exercise = Exam_item + - content :: "(Question) list" + content :: "(Task) list" concerns :: "ContentClass set" <= "{examiner,validator,student}"