equal
deleted
inserted
replaced
203 Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"), |
203 Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"), |
204 |
204 |
205 Thm ("rat_power", num_str @{thm rat_power}) |
205 Thm ("rat_power", num_str @{thm rat_power}) |
206 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*) |
206 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*) |
207 ], |
207 ], |
208 scr = Script ((term_of o the o (parse thy)) "empty_script") |
208 scr = Prog ((term_of o the o (parse thy)) "empty_script") |
209 }), |
209 }), |
210 Rls_ make_rat_poly_with_parentheses, |
210 Rls_ make_rat_poly_with_parentheses, |
211 Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*) |
211 Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*) |
212 Rls_ rat_reduce_1 |
212 Rls_ rat_reduce_1 |
213 ], |
213 ], |
214 scr = Script ((term_of o the o (parse thy)) "empty_script") |
214 scr = Prog ((term_of o the o (parse thy)) "empty_script") |
215 }:rls; |
215 }:rls; |
216 |
216 |
217 (*.for simplify_Integral adapted from 'norm_Rational'.*) |
217 (*.for simplify_Integral adapted from 'norm_Rational'.*) |
218 val norm_Rational_noadd_fractions = |
218 val norm_Rational_noadd_fractions = |
219 Seq {id = "norm_Rational_noadd_fractions", preconds = [], |
219 Seq {id = "norm_Rational_noadd_fractions", preconds = [], |
224 Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*) |
224 Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*) |
225 Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*) |
225 Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*) |
226 Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *) |
226 Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *) |
227 Rls_ discard_parentheses1 (* mult only *) |
227 Rls_ discard_parentheses1 (* mult only *) |
228 ], |
228 ], |
229 scr = Script ((term_of o the o (parse thy)) "empty_script") |
229 scr = Prog ((term_of o the o (parse thy)) "empty_script") |
230 }:rls; |
230 }:rls; |
231 |
231 |
232 (*.simplify terms before and after Integration such that |
232 (*.simplify terms before and after Integration such that |
233 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO |
233 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO |
234 common denominator as done by norm_Rational or make_ratpoly_in. |
234 common denominator as done by norm_Rational or make_ratpoly_in. |