From 01dac36275deebfd33b8136a7808bb4dfe8ea72a Mon Sep 17 00:00:00 2001 From: Idir AIT SADOUNE Date: Fri, 27 Apr 2018 11:15:27 +0200 Subject: [PATCH] no message --- examples/simple/Article.thy | 2 +- examples/simple/MathExam.thy | 22 +++++----------------- ontologies/mathex_onto.thy | 1 + 3 files changed, 7 insertions(+), 18 deletions(-) diff --git a/examples/simple/Article.thy b/examples/simple/Article.thy index f3567783..8339fa11 100644 --- a/examples/simple/Article.thy +++ b/examples/simple/Article.thy @@ -11,7 +11,7 @@ text*[tit::title]{* Using The Isabelle Ontology Framework*} text*[stit::subtitle] \Linking the Formal with the Informal\ text*[auth1::author, affiliation="''University of Sheffield''"]\Achim Brucker\ -text*[auth2::author, affiliation="''Centrale-Supelec''"]\Idir Ait-Adune\ +text*[auth2::author, affiliation="''Centrale-Supelec''"]\Idir Ait-Sadoune\ text*[auth3::author, affiliation="''IRT-SystemX''"]\Paolo Crizzifulli\ text*[auth4::author, affiliation="''Universit\\'e Paris-Sud''"]\Burkhart Wolff\ term "\author.tag_attribute=undefined,affiliation=undefined\" diff --git a/examples/simple/MathExam.thy b/examples/simple/MathExam.thy index 91d82fa2..5dfd23fa 100644 --- a/examples/simple/MathExam.thy +++ b/examples/simple/MathExam.thy @@ -4,12 +4,12 @@ begin open_monitor*[exam::MathExam] -text*[idir::Author, affiliation="''CentraleSupelec''"]{*Idir AIT SADOUNE*} +text*[idir::Author, affiliation="CentraleSupelec"]{*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 +19,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. -*} -*) \ No newline at end of file diff --git a/ontologies/mathex_onto.thy b/ontologies/mathex_onto.thy index b617f9cc..51b9d709 100644 --- a/ontologies/mathex_onto.thy +++ b/ontologies/mathex_onto.thy @@ -26,6 +26,7 @@ doc_class Question = doc_class Exercise= content :: "(Question) list" + mark :: integer doc_class MathExam= content :: "(Header + Author + Exercise) list"