Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF

examples/simple/MathExam.thy

@@ -4,12 +4,13 @@ begin
 
 open_monitor*[exam::MathExam] 
 
-text*[idir::Author, affiliation="''CentraleSupelec''"]{*Idir AIT SADOUNE*}
+text*[idir::Author, affiliation="''CentraleSupelec''", email="''idir.aitsadoune@centralesupelec.fr''"]
+{*Idir AIT SADOUNE*}
 
-text*[header::Header,examGrade="A1", examSubject= "algebra", examTitle="''Exam number 1''"]
+text*[header::Header,examGrade="A1", examSubject= "algebra", examTitle="Exam number 1"]
 {* Please follow directions carefully and show all your work.*}
 
-section*[exo1 :: Exercise, content="[q1,q2,q3]"]{* Exercise 1.*}
+section*[exo1 :: Exercise, content="[q1,q2,q3]", mark="15"]{* Exercise 1.*}
 text*[q1::Question, level="twoStars", mark="5"] 
 {*
 Give an example of each of the following : 
@@ -19,24 +20,12 @@ b - a real number which is not rational.
 
 text*[q2::Question, level="oneStar", mark="5"] 
 {*
-Write in interval notation : @{term ''-3 < x < 5''}
+Write in interval notation : @{term "-3 < x"} and  @{term "x < 5"}
 *}
 
 text*[q3::Question, level="oneStar", mark="5"] 
-{* True or false : @{term ''0/8 = 0''} *}
+{* True or false : @{term "0/8 = 0"} *}
 
 close_monitor*[exam] 
 
 end
-
-(*
-
-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.
-*}
-*)

ontologies/mathex_onto.thy

@@ -5,6 +5,7 @@ begin
 
 doc_class Author =
    affiliation :: "string"
+  email :: "string"
 
 datatype Subject =
   algebra | geometry | statistical
@@ -26,12 +27,11 @@ doc_class Question =
 
 doc_class Exercise= 
   content :: "(Question) list"
+  mark :: integer
 
 doc_class MathExam=
   content :: "(Header + Author + Exercise) list"
   where "((Author)+  ~
           Header ~ 
          (Exercise)+ )"
-  
-  
 end