340 setup {* KEStore_Elems.add_pbts |
340 setup {* KEStore_Elems.add_pbts |
341 [(Specify.prep_pbt thy "pbl_fun_integ" [] Celem.e_pblID |
341 [(Specify.prep_pbt thy "pbl_fun_integ" [] Celem.e_pblID |
342 (["integrate","function"], |
342 (["integrate","function"], |
343 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
343 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
344 ("#Find" ,["antiDerivative F_F"])], |
344 ("#Find" ,["antiDerivative F_F"])], |
345 Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], |
345 Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], |
346 SOME "Integrate (f_f, v_v)", |
346 SOME "Integrate (f_f, v_v)", |
347 [["diff","integration"]])), |
347 [["diff","integration"]])), |
348 (*here "named" is used differently from Differentiation"*) |
348 (*here "named" is used differently from Differentiation"*) |
349 (Specify.prep_pbt thy "pbl_fun_integ_nam" [] Celem.e_pblID |
349 (Specify.prep_pbt thy "pbl_fun_integ_nam" [] Celem.e_pblID |
350 (["named","integrate","function"], |
350 (["named","integrate","function"], |
351 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
351 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
352 ("#Find" ,["antiDerivativeName F_F"])], |
352 ("#Find" ,["antiDerivativeName F_F"])], |
353 Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], |
353 Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], |
354 SOME "Integrate (f_f, v_v)", |
354 SOME "Integrate (f_f, v_v)", |
355 [["diff","integration","named"]]))] *} |
355 [["diff","integration","named"]]))] *} |
356 |
356 |
357 (** methods **) |
357 (** methods **) |
358 setup {* KEStore_Elems.add_mets |
358 setup {* KEStore_Elems.add_mets |