455 rules = [Thm ("real_assoc_1",num_str @{thm real_assoc_1}), |
455 rules = [Thm ("real_assoc_1",num_str @{thm real_assoc_1}), |
456 Thm ("real_assoc_2",num_str @{thm real_assoc_2}), |
456 Thm ("real_assoc_2",num_str @{thm real_assoc_2}), |
457 Thm ("real_diff_minus",num_str @{thm real_diff_minus}), |
457 Thm ("real_diff_minus",num_str @{thm real_diff_minus}), |
458 Thm ("real_unari_minus",num_str @{thm real_unari_minus}), |
458 Thm ("real_unari_minus",num_str @{thm real_unari_minus}), |
459 Thm ("realpow_multI",num_str @{thm realpow_multI}), |
459 Thm ("realpow_multI",num_str @{thm realpow_multI}), |
460 Calc ("op +",eval_binop "#add_"), |
460 Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
461 Calc ("op -",eval_binop "#sub_"), |
461 Calc ("Groups.minus_class.minus",eval_binop "#sub_"), |
462 Calc ("op *",eval_binop "#mult_"), |
462 Calc ("op *",eval_binop "#mult_"), |
463 Calc ("HOL.divide", eval_cancel "#divide_e"), |
463 Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"), |
464 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), |
464 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), |
465 Calc ("Atools.pow" ,eval_binop "#power_"), |
465 Calc ("Atools.pow" ,eval_binop "#power_"), |
466 Rls_ reduce_012 |
466 Rls_ reduce_012 |
467 ], |
467 ], |
468 scr = Script ((term_of o the o (parse thy)) "empty_script") |
468 scr = Script ((term_of o the o (parse thy)) "empty_script") |
1479 Rls_ order_add_mult_in, |
1479 Rls_ order_add_mult_in, |
1480 Rls_ discard_parentheses, |
1480 Rls_ discard_parentheses, |
1481 Rls_ separate_bdvs, |
1481 Rls_ separate_bdvs, |
1482 (* Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*) |
1482 (* Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*) |
1483 Rls_ cancel_p |
1483 Rls_ cancel_p |
1484 (*Calc ("HOL.divide" ,eval_cancel "#divide_e") too weak!*) |
1484 (*Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e") too weak!*) |
1485 ], |
1485 ], |
1486 scr = EmptyScr}:rls); |
1486 scr = EmptyScr}:rls); |
1487 |
1487 |
1488 |
1488 |
1489 ruleset' := overwritelthy @{theory} (!ruleset', |
1489 ruleset' := overwritelthy @{theory} (!ruleset', |