equal
deleted
inserted
replaced
180 ], |
180 ], |
181 append_rls "e_rls" e_rls [(*for preds in where_ TODO*)], |
181 append_rls "e_rls" e_rls [(*for preds in where_ TODO*)], |
182 NONE, |
182 NONE, |
183 [["simplification","of_rationals","to_partial_fraction"]])); |
183 [["simplification","of_rationals","to_partial_fraction"]])); |
184 *} |
184 *} |
185 setup {* KEStore_Elems.store_pbts |
185 setup {* KEStore_Elems.add_pbts |
186 [(prep_pbt @{theory} "pbl_simp_rat_partfrac" [] e_pblID |
186 [(prep_pbt @{theory} "pbl_simp_rat_partfrac" [] e_pblID |
187 (["partial_fraction", "rational", "simplification"], |
187 (["partial_fraction", "rational", "simplification"], |
188 [("#Given" ,["functionTerm t_t", "solveFor v_v"]), |
188 [("#Given" ,["functionTerm t_t", "solveFor v_v"]), |
189 (* TODO: call this sub-problem with appropriate functionTerm: |
189 (* TODO: call this sub-problem with appropriate functionTerm: |
190 leading coefficient of the denominator is 1: to be checked here! and.. |
190 leading coefficient of the denominator is 1: to be checked here! and.. |