270 ("#Find" ,["derivativeEq f_f'"]) |
270 ("#Find" ,["derivativeEq f_f'"]) |
271 ], |
271 ], |
272 append_rls "e_rls" e_rls [], |
272 append_rls "e_rls" e_rls [], |
273 SOME "Differentiate (f_f, v_v)", [["diff","differentiate_equality"]])); |
273 SOME "Differentiate (f_f, v_v)", [["diff","differentiate_equality"]])); |
274 *} |
274 *} |
275 setup {* KEStore_Elems.store_pbts |
275 setup {* KEStore_Elems.add_pbts |
276 [(prep_pbt thy "pbl_fun" [] e_pblID (["function"], [], e_rls, NONE, [])), |
276 [(prep_pbt thy "pbl_fun" [] e_pblID (["function"], [], e_rls, NONE, [])), |
277 (prep_pbt thy "pbl_fun_deriv" [] e_pblID |
277 (prep_pbt thy "pbl_fun_deriv" [] e_pblID |
278 (["derivative_of","function"], |
278 (["derivative_of","function"], |
279 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]), |
279 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]), |
280 ("#Find" ,["derivative f_f'"])], |
280 ("#Find" ,["derivative f_f'"])], |