diff --git a/examples/math_exam/BAC2017.thy b/examples/math_exam/BAC2017.thy
index 9ba4a9a..30ce30f 100644
--- a/examples/math_exam/BAC2017.thy
+++ b/examples/math_exam/BAC2017.thy
@@ -1,15 +1,19 @@
 theory BAC2017
   imports "../../ontologies/mathex_onto"
-    Real
+    Deriv Transcendental
 begin
    
 open_monitor*[exam::MathExam] 
 
-section*[idir::Author,affiliation="''CentraleSupelec''", 
+section*[idir::Author,affiliation="''LRI, CentraleSupelec''", 
 email="''idir.aitsadoune@centralesupelec.fr''"]
 {*Idir AIT SADOUNE*}
 
-section*[header::Header,examSubject= "[algebra,geometry]", 
+section*[keller::Author,affiliation="''LRI, Univ. Paris-Sud''", 
+email="''Chantal.Keller@lri.fr''"]
+{*Chantal KELLER*}
+
+subsection*[header::Header,examSubject= "[algebra,geometry]", 
  examTitle="''BACCALAUREAT GENERAL MATHEMATIQUES''", 
 date="''21-06-2017''", 
 timeAllowed="240::int"]
@@ -23,21 +27,72 @@ timeAllowed="240::int"]
 \end{itemize}
 *}
 
-section*[exo1 :: Exercise,Exercise.concerns= "{examiner,validator,student}",
-Exercise.content="[q1::Task]"]
+subsubsection*[exo1 :: Exercise,Exercise.concerns= "{examiner,validator,student}",
+Exercise.content="[q1::Task,q2,q3a]"]
 {* 
-On considère la fonction h définie sur l’intervalle [0..+\<infinity>] par : @{term "h(x) = x * e^(-x)"}
+On considère la fonction h définie sur l’intervalle [0..+\<infinity>] par : @{term "h(x) = x * exponent (-x)"}
 *}
 
+definition h :: "real \<Rightarrow> real"
+  where "h x \<equiv> x * exp (- x)"
+
   
-subsection*[q1::Task, Task.concerns= "{examiner,validator,student}",
-subitems="[q11]",
+subsubsection*[q1::Task, Task.concerns= "{examiner,validator,student}",
 level="oneStar", mark="1::int", type="formal"] 
-{* Déterminer la limite de la fonction h en +\<infinity>. *}
+{* Déterminer la limite de la fonction @{term h} en +\<infinity>. *}
 
-text*[q11::Answer_Formal_Step]
-{* First Step: Fill in term and justifi*}
+text*[a1::Answer_Formal_Step]
+{* Fill in term and justification*}
 
+lemma q1 : "(h \<longlongrightarrow> (0::real)) at_top"
+  sorry
+
+  
+subsubsection*[q2::Task, Task.concerns= "{examiner,validator,student}",
+level="oneStar", mark="1::int", type="formal"] 
+{* Étudier les variations de la fonction @{term h} sur l'intervalle [0..+\<infinity>] et dresser son tableau
+   de variation *}
+
+
+text*[a2::Answer_Formal_Step]
+{* Fill in term and justification*}
+
+
+definition h' :: "real \<Rightarrow> real"
+  where "h' x \<equiv> (1 - x) * exp (- x)"
+
+lemma q2_a : "DERIV h x :> h' x"
+proof -
+  have * : "DERIV (exp \<circ> uminus) x :> - (exp (-x))"
+    by (simp add: has_derivative_compose)
+  have ** : "DERIV id x :> 1"
+    by (metis DERIV_ident eq_id_iff)
+  have *** : "DERIV h x :> x * (- (exp (- x))) + 1 * (exp (- x))"
+    by (simp add: * ** has_derivative_mult comp_def)
+  show ?thesis
+    by (metis "***" left_diff_distrib mult_minus_right uminus_add_conv_diff)
+qed
+
+
+lemma q2_b : "0 \<le> x \<and> x \<le> y \<and> y \<le> 1 \<Longrightarrow> h x \<le> h y"
+  sorry
+
+
+lemma q2_c : "1 \<le> x \<and> x \<le> y \<Longrightarrow> h x \<ge> h y"
+  sorry
+
+
+subsubsection*[q3a::Task, Task.concerns= "{examiner,validator,student}",
+level="oneStar", mark="1::int", type="formal"] 
+{* Vérifier que pour tout nombre réel x appartenant à l'intervalle [0..+\<infinity>], on a :
+   @term{h x = (exp (- x)) - (h' x)} *}
+
+lemma q3a : "h x = (exp (- x)) - (h' x)"
+  by (simp add : h_def h'_def left_diff_distrib)
+
+
+text*[a3a::Answer_Formal_Step]
+{* Fill in term and justification*}
 
 
 close_monitor*[exam] 
diff --git a/examples/scholarly/Article.thy b/examples/scholarly/Article.thy
index d01fbc2..588205e 100644
--- a/examples/scholarly/Article.thy
+++ b/examples/scholarly/Article.thy
@@ -50,17 +50,21 @@ Thm.concl_of;
   
 ML{* 
 val X =  (@{term scholarly_paper.example.comment})
-val Y = Type.legacy_freeze @{docitem_value \<open>bgrnd\<close>}
+val Y = Type.legacy_freeze @{docitem_value \<open>bgrnd\<close>};
+Syntax.string_of_term
 *}
 ML{* 
 fun calculate_attr_access ctxt f term =
-    let val term = Type.legacy_freeze term;
-        val ty = type_of term
+    (* term assumed to be ground type, (f term) not necessarily *)
+    let val _ = writeln("XXX"^(Syntax.string_of_term ctxt term))
+        val [subterm'] = Type_Infer_Context.infer_types ctxt [f term]
+        val ty = type_of (subterm')
+        val _ = writeln("YYY"^(Syntax.string_of_term ctxt subterm'))
         val term' = (Const(@{const_name "HOL.eq"}, ty --> ty --> HOLogic.boolT) 
-                              $ (Type.legacy_freeze(f term)) 
+                              $ subterm' 
                               $ Free("_XXXXXXX", ty))
-        val term'' = (HOLogic.mk_Trueprop(term'))
-        val thm = simplify @{context} (Thm.assume(Thm.cterm_of ctxt term''));
+        val _ = writeln("ZZZ"^(Syntax.string_of_term ctxt term'))
+        val thm = simplify ctxt (Thm.assume(Thm.cterm_of ctxt (HOLogic.mk_Trueprop term')));
         val Const(@{const_name "HOL.eq"},_) $ lhs $ _ = HOLogic.dest_Trueprop (Thm.concl_of thm)
     in  lhs end
 
@@ -69,6 +73,9 @@ val H = fn X => @{term scholarly_paper.example.comment} $ X
 
  *}  
   
+ML{*val t = calculate_attr_access @{context} H @{docitem_value \<open>bgrnd\<close>}; *}  
+  
+  
 term "scholarly_paper.author.affiliation_update"
 term "scholarly_paper.abstract.keywordlist_update"
 term "scholarly_paper.introduction.comment_update"