423 Thm ("radd_real_const",num_str @{thm radd_real_const}), |
423 Thm ("radd_real_const",num_str @{thm radd_real_const}), |
424 (* these 2 rules are invers to distr_div_right wrt. termination. |
424 (* these 2 rules are invers to distr_div_right wrt. termination. |
425 thus they MUST be done IMMEDIATELY before calc *) |
425 thus they MUST be done IMMEDIATELY before calc *) |
426 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
426 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
427 Calc ("Groups.times_class.times", eval_binop "#mult_"), |
427 Calc ("Groups.times_class.times", eval_binop "#mult_"), |
428 Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"), |
428 Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"), |
429 Calc ("Atools.pow", eval_binop "#power_"), |
429 Calc ("Atools.pow", eval_binop "#power_"), |
430 |
430 |
431 Thm ("rcollect_right",num_str @{thm rcollect_right}), |
431 Thm ("rcollect_right",num_str @{thm rcollect_right}), |
432 Thm ("rcollect_one_left",num_str @{thm rcollect_one_left}), |
432 Thm ("rcollect_one_left",num_str @{thm rcollect_one_left}), |
433 Thm ("rcollect_one_left_assoc",num_str @{thm rcollect_one_left_assoc}), |
433 Thm ("rcollect_one_left_assoc",num_str @{thm rcollect_one_left_assoc}), |
501 ("matches",("Tools.matches",eval_matches "#matches_")), |
501 ("matches",("Tools.matches",eval_matches "#matches_")), |
502 ("lhs" ,("Tools.lhs" ,eval_lhs "")), |
502 ("lhs" ,("Tools.lhs" ,eval_lhs "")), |
503 (*aus Atools.ML*) |
503 (*aus Atools.ML*) |
504 ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")), |
504 ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")), |
505 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")), |
505 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")), |
506 ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")), |
506 ("DIVIDE" ,("Fields.inverse_class.divide" ,eval_cancel "#divide_e")), |
507 ("POWER" ,("Atools.pow" ,eval_binop "#power_")), |
507 ("POWER" ,("Atools.pow" ,eval_binop "#power_")), |
508 ("is_const",("Atools.is'_const",eval_const "#is_const_")), |
508 ("is_const",("Atools.is'_const",eval_const "#is_const_")), |
509 ("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")), |
509 ("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")), |
510 ("leq" ,("Orderings.ord_class.less_eq" ,eval_equ "#less_equal_")), |
510 ("leq" ,("Orderings.ord_class.less_eq" ,eval_equ "#less_equal_")), |
511 ("ident" ,("Atools.ident",eval_ident "#ident_")), |
511 ("ident" ,("Atools.ident",eval_ident "#ident_")), |