1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Dec 14 14:20:25 2016 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Sun Dec 18 16:27:41 2016 +0100
1.3 @@ -338,7 +338,7 @@
1.4
1.5 (** problems **)
1.6 setup {* KEStore_Elems.add_pbts
1.7 - [(prep_pbt thy "pbl_fun_integ" [] e_pblID
1.8 + [(Specify.prep_pbt thy "pbl_fun_integ" [] e_pblID
1.9 (["integrate","function"],
1.10 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
1.11 ("#Find" ,["antiDerivative F_F"])],
1.12 @@ -346,7 +346,7 @@
1.13 SOME "Integrate (f_f, v_v)",
1.14 [["diff","integration"]])),
1.15 (*here "named" is used differently from Differentiation"*)
1.16 - (prep_pbt thy "pbl_fun_integ_nam" [] e_pblID
1.17 + (Specify.prep_pbt thy "pbl_fun_integ_nam" [] e_pblID
1.18 (["named","integrate","function"],
1.19 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
1.20 ("#Find" ,["antiDerivativeName F_F"])],
1.21 @@ -356,7 +356,7 @@
1.22
1.23 (** methods **)
1.24 setup {* KEStore_Elems.add_mets
1.25 - [prep_met thy "met_diffint" [] e_metID
1.26 + [Specify.prep_met thy "met_diffint" [] e_metID
1.27 (["diff","integration"],
1.28 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_F"])],
1.29 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = e_rls, prls=e_rls,
1.30 @@ -364,7 +364,7 @@
1.31 "Script IntegrationScript (f_f::real) (v_v::real) = " ^
1.32 " (let t_t = Take (Integral f_f D v_v) " ^
1.33 " in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))"),
1.34 - prep_met thy "met_diffint_named" [] e_metID
1.35 + Specify.prep_met thy "met_diffint_named" [] e_metID
1.36 (["diff","integration","named"],
1.37 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
1.38 ("#Find" ,["antiDerivativeName F_F"])],