270 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO |
270 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO |
271 common denominator as done by norm_Rational or make_ratpoly_in. |
271 common denominator as done by norm_Rational or make_ratpoly_in. |
272 This is a copy from 'make_polynomial_in' with insertions from |
272 This is a copy from 'make_polynomial_in' with insertions from |
273 'make_ratpoly_in' |
273 'make_ratpoly_in' |
274 THIS IS KEPT FOR COMPARISON ............................................ |
274 THIS IS KEPT FOR COMPARISON ............................................ |
275 * val simplify_Integral = prep_rls( |
275 * val simplify_Integral = prep_rls'( |
276 * Seq {id = "", preconds = []:term list, |
276 * Seq {id = "", preconds = []:term list, |
277 * rew_ord = ("dummy_ord", dummy_ord), |
277 * rew_ord = ("dummy_ord", dummy_ord), |
278 * erls = Atools_erls, srls = Erls, |
278 * erls = Atools_erls, srls = Erls, |
279 * calc = [], (*asm_thm = [],*) |
279 * calc = [], (*asm_thm = [],*) |
280 * rules = [Rls_ expand_poly, |
280 * rules = [Rls_ expand_poly, |
319 rules = [ Rls_ integration_rules, |
319 rules = [ Rls_ integration_rules, |
320 Rls_ add_new_c, |
320 Rls_ add_new_c, |
321 Rls_ simplify_Integral |
321 Rls_ simplify_Integral |
322 ], |
322 ], |
323 scr = EmptyScr}; |
323 scr = EmptyScr}; |
|
324 |
|
325 val prep_rls' = prep_rls @{theory}; |
324 *} |
326 *} |
325 setup {* KEStore_Elems.add_rlss |
327 setup {* KEStore_Elems.add_rlss |
326 [("integration_rules", (Context.theory_name @{theory}, prep_rls integration_rules)), |
328 [("integration_rules", (Context.theory_name @{theory}, prep_rls' integration_rules)), |
327 ("add_new_c", (Context.theory_name @{theory}, prep_rls add_new_c)), |
329 ("add_new_c", (Context.theory_name @{theory}, prep_rls' add_new_c)), |
328 ("simplify_Integral", (Context.theory_name @{theory}, prep_rls simplify_Integral)), |
330 ("simplify_Integral", (Context.theory_name @{theory}, prep_rls' simplify_Integral)), |
329 ("integration", (Context.theory_name @{theory}, prep_rls integration)), |
331 ("integration", (Context.theory_name @{theory}, prep_rls' integration)), |
330 ("separate_bdv2", (Context.theory_name @{theory}, prep_rls separate_bdv2)), |
332 ("separate_bdv2", (Context.theory_name @{theory}, prep_rls' separate_bdv2)), |
331 |
333 |
332 ("norm_Rational_noadd_fractions", (Context.theory_name @{theory}, |
334 ("norm_Rational_noadd_fractions", (Context.theory_name @{theory}, |
333 prep_rls norm_Rational_noadd_fractions)), |
335 prep_rls' norm_Rational_noadd_fractions)), |
334 ("norm_Rational_rls_noadd_fractions", (Context.theory_name @{theory}, |
336 ("norm_Rational_rls_noadd_fractions", (Context.theory_name @{theory}, |
335 prep_rls norm_Rational_rls_noadd_fractions))] *} |
337 prep_rls' norm_Rational_rls_noadd_fractions))] *} |
336 |
338 |
337 (** problems **) |
339 (** problems **) |
338 setup {* KEStore_Elems.add_pbts |
340 setup {* KEStore_Elems.add_pbts |
339 [(prep_pbt thy "pbl_fun_integ" [] e_pblID |
341 [(prep_pbt thy "pbl_fun_integ" [] e_pblID |
340 (["integrate","function"], |
342 (["integrate","function"], |