44 Rule_Set.append_rules "LinEq_crls" poly_crls |
44 Rule_Set.append_rules "LinEq_crls" poly_crls |
45 [\<^rule_thm>\<open>real_assoc_1\<close> |
45 [\<^rule_thm>\<open>real_assoc_1\<close> |
46 (* |
46 (* |
47 Don't use |
47 Don't use |
48 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
48 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
49 \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"), |
49 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"), |
50 *) |
50 *) |
51 ]; |
51 ]; |
52 |
52 |
53 (* ----- crls ----- *) |
53 (* ----- crls ----- *) |
54 val LinEq_erls = |
54 val LinEq_erls = |
55 Rule_Set.append_rules "LinEq_erls" Poly_erls [ |
55 Rule_Set.append_rules "LinEq_erls" Poly_erls [ |
56 \<^rule_thm>\<open>real_assoc_1\<close> |
56 \<^rule_thm>\<open>real_assoc_1\<close> |
57 (* |
57 (* |
58 Don't use |
58 Don't use |
59 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
59 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
60 \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"), |
60 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"), |
61 *) |
61 *) |
62 ]; |
62 ]; |
63 \<close> |
63 \<close> |
64 rule_set_knowledge LinEq_erls = LinEq_erls |
64 rule_set_knowledge LinEq_erls = LinEq_erls |
65 ML \<open> |
65 ML \<open> |
70 erls = LinEq_erls, |
70 erls = LinEq_erls, |
71 srls = Rule_Set.Empty, |
71 srls = Rule_Set.Empty, |
72 calc = [], errpatts = [], |
72 calc = [], errpatts = [], |
73 rules = [ |
73 rules = [ |
74 \<^rule_thm>\<open>real_assoc_1\<close>, |
74 \<^rule_thm>\<open>real_assoc_1\<close>, |
75 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
75 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
76 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"), |
76 \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"), |
77 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
77 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"), |
78 (* Don't use |
78 (* Don't use |
79 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
79 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
80 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"), |
80 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"), |
81 *) |
81 *) |
82 \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")], |
82 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")], |
83 scr = Rule.Empty_Prog}); |
83 scr = Rule.Empty_Prog}); |
84 \<close> |
84 \<close> |
85 rule_set_knowledge LinPoly_simplify = LinPoly_simplify |
85 rule_set_knowledge LinPoly_simplify = LinPoly_simplify |
86 ML \<open> |
86 ML \<open> |
87 |
87 |