16 (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'')) (f_f::real))" |
16 (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'')) (f_f::real))" |
17 setup \<open>KEStore_Elems.add_mets |
17 setup \<open>KEStore_Elems.add_mets |
18 [Specify.prep_met @{theory "Isac_Knowledge"} "met_testint" [] Celem.e_metID |
18 [Specify.prep_met @{theory "Isac_Knowledge"} "met_testint" [] Celem.e_metID |
19 (["diff","integration","test"], |
19 (["diff","integration","test"], |
20 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find", ["antiDerivative F_F"])], |
20 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find", ["antiDerivative F_F"])], |
21 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, |
21 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.e_rls, prls = Rule_Set.e_rls, |
22 crls = Atools_erls, errpats = [], nrls = Rule.e_rls}, |
22 crls = Atools_erls, errpats = [], nrls = Rule_Set.e_rls}, |
23 @{thm integration_test.simps})]\<close> |
23 @{thm integration_test.simps})]\<close> |
24 |
24 |
25 end |
25 end |