2018-04-06 12:25:21 +00:00
|
|
|
theory mathex_onto
|
|
|
|
|
|
|
|
|
|
imports "../Isa_DOF"
|
|
|
|
|
begin
|
|
|
|
|
|
2018-04-06 12:32:22 +00:00
|
|
|
doc_class Question =
|
2018-04-06 12:48:43 +00:00
|
|
|
content :: "(string + term) list"
|
2018-04-06 12:32:22 +00:00
|
|
|
|
|
|
|
|
doc_class Response =
|
2018-04-06 12:48:43 +00:00
|
|
|
content :: "(string + term) list"
|
2018-04-06 12:32:22 +00:00
|
|
|
|
2018-04-06 12:48:43 +00:00
|
|
|
doc_class Exercise_part =
|
2018-04-06 12:32:22 +00:00
|
|
|
question :: Question
|
|
|
|
|
response :: Response
|
|
|
|
|
|
2018-04-06 12:48:43 +00:00
|
|
|
doc_class Exercise=
|
|
|
|
|
content :: "(Exercise_part) list"
|
2018-04-06 12:32:22 +00:00
|
|
|
|
2018-04-06 12:25:21 +00:00
|
|
|
end
|
