From 2e185d9c25f2573f2ec255cc5320bb7f8322291d Mon Sep 17 00:00:00 2001
From: Idir AIT SADOUNE <idir.aitsadoune@centralesupelec.fr>
Date: Wed, 18 Apr 2018 09:36:21 +0200
Subject: [PATCH] no message

---
 examples/simple/MathExam.thy | 21 +++++++++++----------
 ontologies/mathex_onto.thy   |  7 ++++---
 2 files changed, 15 insertions(+), 13 deletions(-)

diff --git a/examples/simple/MathExam.thy b/examples/simple/MathExam.thy
index c839cee9..ed9c8b35 100644
--- a/examples/simple/MathExam.thy
+++ b/examples/simple/MathExam.thy
@@ -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
\ No newline at end of file
+*)
\ No newline at end of file
diff --git a/ontologies/mathex_onto.thy b/ontologies/mathex_onto.thy
index ea55d6cd..b617f9cc 100644
--- a/ontologies/mathex_onto.thy
+++ b/ontologies/mathex_onto.thy
@@ -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
\ No newline at end of file