pierre.derathe
/
Isabelle_DOF
Archived
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

sync

This commit is contained in:
Burkhart Wolff 2018-05-01 15:30:37 +02:00
parent 356fec67fe
commit 5820365c12
1 changed files with 13 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
ontologies/mathex_onto.thy
View File

@ -42,14 +42,26 @@ datatype ContentClass =
doc_class Exam_item =
concerns :: "ContentClass set"
datatype SubQuestion = Item string
doc_class Answer_Formal = Exam_item +
step_label :: string
"term" :: "string"
doc_class Answer_YesNo = Exam_item +
step_label :: string
yes_no :: bool -- \<open>for checkboxes\<close>
datatype Question_Type =
formal | informal
formal | informal | mixed
doc_class Question = Exam_item +
level :: Level
type :: Question_Type
subitems :: "(SubQuestion * (Answer_Formal + Answer_YesNo)list) list"
concerns :: "ContentClass set" <= "{examiner,validator,student}"
mark :: int
doc_class Exercise = Exam_item +
content :: "(Question) list"