From ce17b1cf58280df4d89a919eb95c59c3234089c8 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Tue, 29 May 2018 12:02:13 +0200
Subject: [PATCH] Repaired MathExam wrt. Ontology.

---
 examples/math_exam/MathExam.thy | 25 ++++++++++++++++++++++---
 1 file changed, 22 insertions(+), 3 deletions(-)

diff --git a/examples/math_exam/MathExam.thy b/examples/math_exam/MathExam.thy
index d80493a..929c5a1 100644
--- a/examples/math_exam/MathExam.thy
+++ b/examples/math_exam/MathExam.thy
@@ -1,5 +1,6 @@
 theory MathExam
   imports "../../ontologies/mathex_onto"
+    Real
 begin
    
 open_monitor*[exam::MathExam] 
@@ -18,7 +19,13 @@ subsection*[header::Header,examSubject= "algebra",  examTitle="''Exam number 1''
 \end{itemize}
 *}
 
-subsubsection*[exo1 :: Exercise, Exercise.content="[q1::Question,q2::Question]"]
+(*
+text*[fig1::figure, width = "Some(textwidth 80)", 
+      "file"="@{file ''../../../figures/Dogfood-Intro.png''}"]
+     {* Ouroboros I : This paper from inside ... *}  
+*)
+
+subsubsection*[exo1 :: Exercise, Exercise.content="[q1::Task,q2::Task]"]
 {* 
 Here are the first four lines of a number pattern.
 \begin{itemize}
@@ -29,12 +36,24 @@ Here are the first four lines of a number pattern.
 \end{itemize}
 *}
 
-text*[q1::Question, level="oneStar", Question.mark="1::int", type="formal"] 
+lemma XX : "(x ^ 3) + 2 * (x^2) + 11 * x - 12 = (x-4) * (x+1) * (x - 3)"
+proof -
+  have  " (x ^ 3) + 2 * (x^2) + 11 * x - 12 = (x + 1) * ( x ^ 2 - 2 * x - 3)"
+    sorry
+  have "... = (x + 1) * (x + 4) * (x - 3)"
+    sorry
+  show ?thesis
+    sorry
+qed
+  
+
+  
+text*[q1::Task, level="oneStar", mark="1::int", type="formal"] 
 {*
 Complete Line 10 :  @{term "10*x + 2*y =  11*16"}
 *}
 
-text*[q2::Question, level="threeStars", Question.mark="3::int", type="formal"] 
+text*[q2::Task, level="threeStars", mark="3::int", type="formal"] 
 {*
 Prove that  @{term "n*(n+5) + 2*(n+3) "} is always the product of two numbers with a difference of 5.
 *}