forked from Isabelle_DOF/Isabelle_DOF
parent
325b45834c
commit
be04e99c2f
|
@ -9,6 +9,8 @@ doc_class Question =
|
|||
doc_class Response =
|
||||
content :: "(string + term) list"
|
||||
|
||||
datatype grades = A | B | C
|
||||
|
||||
doc_class Exercise_part =
|
||||
question :: Question
|
||||
response :: Response
|
||||
|
@ -19,4 +21,15 @@ doc_class Exercise=
|
|||
doc_class MathExam=
|
||||
content :: "(Exercise) list"
|
||||
|
||||
section{* Example*}
|
||||
|
||||
term "[ @{thm ''refl''}] @ [ @{thm ''sym''}, @{thm ''trans''} ] "
|
||||
|
||||
text{*
|
||||
@{term "[ @{thm ''refl''}] @ [ @{thm ''sym''}, @{thm ''trans''} ]"}} are the theorems
|
||||
of the equational logic fragment of HOL.
|
||||
*}
|
||||
|
||||
|
||||
|
||||
end
|
Reference in New Issue