458 Thm ("real_diff_minus",num_str @{thm real_diff_minus}), |
458 Thm ("real_diff_minus",num_str @{thm real_diff_minus}), |
459 Thm ("real_unari_minus",num_str @{thm real_unari_minus}), |
459 Thm ("real_unari_minus",num_str @{thm real_unari_minus}), |
460 Thm ("realpow_multI",num_str @{thm realpow_multI}), |
460 Thm ("realpow_multI",num_str @{thm realpow_multI}), |
461 Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
461 Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
462 Calc ("Groups.minus_class.minus",eval_binop "#sub_"), |
462 Calc ("Groups.minus_class.minus",eval_binop "#sub_"), |
463 Calc ("op *",eval_binop "#mult_"), |
463 Calc ("Groups.times_class.times",eval_binop "#mult_"), |
464 Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"), |
464 Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"), |
465 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), |
465 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), |
466 Calc ("Atools.pow" ,eval_binop "#power_"), |
466 Calc ("Atools.pow" ,eval_binop "#power_"), |
467 Rls_ reduce_012 |
467 Rls_ reduce_012 |
468 ], |
468 ], |