53 val LinEq_crls = |
53 val LinEq_crls = |
54 append_rls "LinEq_crls" poly_crls |
54 append_rls "LinEq_crls" poly_crls |
55 [Thm ("real_assoc_1",num_str @{thm real_assoc_1}) |
55 [Thm ("real_assoc_1",num_str @{thm real_assoc_1}) |
56 (* |
56 (* |
57 Don't use |
57 Don't use |
58 Calc ("HOL.divide", eval_cancel "#divide_e"), |
58 Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"), |
59 Calc ("Atools.pow" ,eval_binop "#power_"), |
59 Calc ("Atools.pow" ,eval_binop "#power_"), |
60 *) |
60 *) |
61 ]; |
61 ]; |
62 |
62 |
63 (* ----- crls ----- *) |
63 (* ----- crls ----- *) |
64 val LinEq_erls = |
64 val LinEq_erls = |
65 append_rls "LinEq_erls" Poly_erls |
65 append_rls "LinEq_erls" Poly_erls |
66 [Thm ("real_assoc_1",num_str @{thm real_assoc_1}) |
66 [Thm ("real_assoc_1",num_str @{thm real_assoc_1}) |
67 (* |
67 (* |
68 Don't use |
68 Don't use |
69 Calc ("HOL.divide", eval_cancel "#divide_e"), |
69 Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"), |
70 Calc ("Atools.pow" ,eval_binop "#power_"), |
70 Calc ("Atools.pow" ,eval_binop "#power_"), |
71 *) |
71 *) |
72 ]; |
72 ]; |
73 |
73 |
74 ruleset' := overwritelthy @{theory} (!ruleset', |
74 ruleset' := overwritelthy @{theory} (!ruleset', |
82 srls = Erls, |
82 srls = Erls, |
83 calc = [], |
83 calc = [], |
84 (*asm_thm = [],*) |
84 (*asm_thm = [],*) |
85 rules = [ |
85 rules = [ |
86 Thm ("real_assoc_1",num_str @{thm real_assoc_1}), |
86 Thm ("real_assoc_1",num_str @{thm real_assoc_1}), |
87 Calc ("op +",eval_binop "#add_"), |
87 Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
88 Calc ("op -",eval_binop "#sub_"), |
88 Calc ("Groups.minus_class.minus",eval_binop "#sub_"), |
89 Calc ("op *",eval_binop "#mult_"), |
89 Calc ("op *",eval_binop "#mult_"), |
90 (* Dont use |
90 (* Dont use |
91 Calc ("HOL.divide", eval_cancel "#divide_e"), |
91 Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"), |
92 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), |
92 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), |
93 *) |
93 *) |
94 Calc ("Atools.pow" ,eval_binop "#power_") |
94 Calc ("Atools.pow" ,eval_binop "#power_") |
95 ], |
95 ], |
96 scr = EmptyScr}:rls); |
96 scr = EmptyScr}:rls); |