src/Tools/isac/Knowledge/Integrate.thy
changeset 60312 35f7b2f61797
parent 60309 70a1d102660d
child 60313 8d89a214aedc
     1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Mon Jun 21 15:50:58 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Mon Jun 21 16:18:27 2021 +0200
     1.3 @@ -103,8 +103,8 @@
     1.4    | eval_is_f_x _ _ _ _ = NONE;
     1.5  \<close>
     1.6  setup \<open>KEStore_Elems.add_calcs
     1.7 -  [("add_new_c", ("Integrate.add_new_c", eval_add_new_c "add_new_c_")),
     1.8 -    ("is_f_x", ("Integrate.is_f_x", eval_is_f_x "is_f_idextifier_"))]\<close>
     1.9 +  [("add_new_c", ("Integrate.add_new_c" (* FIXME proper const!? *), eval_add_new_c "add_new_c_")),
    1.10 +    ("is_f_x", (\<^const_name>\<open>is_f_x\<close>, eval_is_f_x "is_f_idextifier_"))]\<close>
    1.11  ML \<open>
    1.12  (** rulesets **)
    1.13