forked from Isabelle_DOF/Isabelle_DOF
no message
This commit is contained in:
parent
baa3ee9b45
commit
2e185d9c25
|
@ -4,29 +4,34 @@ begin
|
|||
|
||||
open_monitor*[exam::MathExam]
|
||||
|
||||
text*[header::Header,examGrade=A1, examSubject= algebra]{*Exam number 1*}
|
||||
text*[idir::Author, affiliation="CentraleSupelec"]{*Idir AIT SADOUNE*}
|
||||
|
||||
section*[exo1 :: Exercise, content="[q1,q2,q3]"]
|
||||
text*[header::Header,examGrade="A1", examSubject= "algebra", examTitle="Exam number 1"]
|
||||
{* Please follow directions carefully ans show all your work.*}
|
||||
|
||||
text*[q1::Question, level=twoStars, mark=5]
|
||||
|
||||
section*[exo1 :: Exercise, content="[q1,q2,q3]"]{* Exercise 1.*}
|
||||
text*[q1::Question, level="twoStars", mark="5"]
|
||||
{*
|
||||
Give an example of each of the following :
|
||||
a - a rational number which is not integer.
|
||||
b - a real number which is not rational.
|
||||
*}
|
||||
|
||||
text*[q2::Question, level=oneStar, mark=5]
|
||||
text*[q2::Question, level="oneStar", mark="5"]
|
||||
{*
|
||||
Write in interval notation : @{term ''-3 < x < 5''}
|
||||
*}
|
||||
|
||||
text*[q3::Question, level=oneStar, mark=5]
|
||||
text*[q3::Question, level="oneStar", mark="5"]
|
||||
{*
|
||||
True or false : @{term ''0/8 = 0''}
|
||||
*}
|
||||
|
||||
close_monitor*[exam]
|
||||
|
||||
end
|
||||
|
||||
(*
|
||||
|
||||
section{* Example*}
|
||||
|
@ -37,8 +42,4 @@ text{*
|
|||
@{term "[ @{thm ''refl''}] @ [ @{thm ''sym''}, @{thm ''trans''} ]"}} are the theorems
|
||||
of the equational logic fragment of HOL.
|
||||
*}
|
||||
*)
|
||||
|
||||
close_monitor*[exam]
|
||||
|
||||
end
|
||||
*)
|
|
@ -16,6 +16,7 @@ datatype Grade =
|
|||
A1 | A2 | A3
|
||||
|
||||
doc_class Header =
|
||||
examTitle :: string
|
||||
examGrade :: Grade
|
||||
examSubject :: Subject
|
||||
|
||||
|
@ -28,9 +29,9 @@ doc_class Exercise=
|
|||
|
||||
doc_class MathExam=
|
||||
content :: "(Header + Author + Exercise) list"
|
||||
where "(Header ~
|
||||
(Author)+ ~
|
||||
(Exercise)+ )"
|
||||
where "((Author)+ ~
|
||||
Header ~
|
||||
(Exercise)+ )"
|
||||
|
||||
|
||||
end
|
Loading…
Reference in New Issue