From d3d7bd760972fc04443f363ecee73c96d695d3fc Mon Sep 17 00:00:00 2001
From: Idir AIT SADOUNE <idir.aitsadoune@centralesupelec.fr>
Date: Tue, 17 Apr 2018 16:42:45 +0200
Subject: [PATCH 1/2] no message

---
 ontologies/mathex_onto.thy | 45 +++++++++++++++++++-------------------
 1 file changed, 23 insertions(+), 22 deletions(-)

diff --git a/ontologies/mathex_onto.thy b/ontologies/mathex_onto.thy
index 507e97d..ea55d6c 100644
--- a/ontologies/mathex_onto.thy
+++ b/ontologies/mathex_onto.thy
@@ -3,33 +3,34 @@ theory mathex_onto
 imports "../Isa_DOF"
 begin
 
+doc_class Author =
+   affiliation :: "string"
+
+datatype Subject =
+  algebra | geometry | statistical
+
+datatype Level =
+  oneStar | twoStars | threeStars
+
+datatype Grade =
+  A1 | A2 | A3
+
+doc_class Header = 
+  examGrade :: Grade
+  examSubject :: Subject
+
 doc_class Question =
-  content :: "(string + term) list"
-
-doc_class Response =
-  content :: "(string + term) list"
-
-datatype grades = A | B | C  
-  
-doc_class Exercise_part = 
-  question :: Question
-  response :: Response
+  level :: Level
+  mark :: integer
 
 doc_class Exercise= 
-  content :: "(Exercise_part) list"
+  content :: "(Question) list"
 
 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.
-*}
-
+  content :: "(Header + Author + Exercise) list"
+ where "(Header ~ 
+        (Author)+  ~
+        (Exercise)+ )"
   
   
 end
\ No newline at end of file

From baa3ee9b45bf26bdb88df68ddf88262958399811 Mon Sep 17 00:00:00 2001
From: Idir AIT SADOUNE <idir.aitsadoune@centralesupelec.fr>
Date: Tue, 17 Apr 2018 16:43:08 +0200
Subject: [PATCH 2/2] no message

---
 examples/simple/MathExam.thy | 44 ++++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)
 create mode 100644 examples/simple/MathExam.thy

diff --git a/examples/simple/MathExam.thy b/examples/simple/MathExam.thy
new file mode 100644
index 0000000..c839cee
--- /dev/null
+++ b/examples/simple/MathExam.thy
@@ -0,0 +1,44 @@
+theory MathExam
+  imports "../../ontologies/mathex_onto"
+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]"]
+{* Please follow directions carefully ans show all your work.*}
+
+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] 
+{*
+Write in interval notation : @{term ''-3 < x < 5''}
+*}
+
+text*[q3::Question, level=oneStar, mark=5] 
+{*
+True or false : @{term ''0/8 = 0''}
+*}
+
+(*
+
+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.
+*}
+*)  
+
+close_monitor*[exam] 
+
+end
\ No newline at end of file