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

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

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