1.1 --- a/TODO.md	Tue Aug 10 13:40:03 2021 +0200
     1.2 +++ b/TODO.md	Tue Aug 10 19:05:59 2021 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    (Exception: rlss with its special cross-theory merge.)
     1.5  
     1.6  * What is the purpose of "#numeral" instead of plain numeral?
     1.7 +    ??
     1.8  
     1.9  * Check/clarify Context.theory_name vs. Context.theory_long_name.
    1.10  
    1.11 @@ -33,8 +34,6 @@
    1.12      "course designer (Kurs-Designer)". The latter just adds examples which re-use existing
    1.13      knowledge designed by the former. KEStore_Elems.add_thes is an interface for the latter.   
    1.14  
    1.15 -* WN: clarify add_calcs with non-existant constant "Integrate.add_new_c";
    1.16 -
    1.17  * WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations,
    1.18    e.g. "Tactical.Try" vs. "Lucas_Interpreter.Try";
    1.19  

     2.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Tue Aug 10 13:40:03 2021 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Tue Aug 10 19:05:59 2021 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  consts
     2.5  
     2.6    Integral            :: "[real, real]=> real" ("Integral _ D _" 91)
     2.7 -(*new_c	      :: "real => real"        ("new_c _" 66)*)
     2.8 +  add_new_c          :: "real => real"        ("add'_new'_c _" 66) 
     2.9    is_f_x            :: "real => bool"        ("_ is'_f'_x" 10)
    2.10  
    2.11    (*descriptions in the related problems*)
    2.12 @@ -102,8 +102,8 @@
    2.13  	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
    2.14    | eval_is_f_x _ _ _ _ = NONE;
    2.15  \<close>
    2.16 -setup \<open>KEStore_Elems.add_calcs
    2.17 -  [("add_new_c", ("Integrate.add_new_c" (* FIXME proper const!? *), eval_add_new_c "add_new_c_"))]\<close>
    2.18 +
    2.19 +calculation add_new_c = \<open>eval_add_new_c "add_new_c_"\<close>
    2.20  calculation is_f_x = \<open>eval_is_f_x "is_f_idextifier_"\<close>
    2.21  
    2.22  ML \<open>