170 Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"), |
170 Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"), |
171 Calc ("Rings.inverse_class.divide",eval_cancel "#divide_e"), |
171 Calc ("Rings.inverse_class.divide",eval_cancel "#divide_e"), |
172 Calc ("Atools.pow" ,eval_binop "#power_"), |
172 Calc ("Atools.pow" ,eval_binop "#power_"), |
173 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
173 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
174 Calc ("Groups.minus_class.minus", eval_binop "#sub_"), |
174 Calc ("Groups.minus_class.minus", eval_binop "#sub_"), |
175 Calc ("op *", eval_binop "#mult_"), |
175 Calc ("Groups.times_class.times", eval_binop "#mult_"), |
176 Calc ("op =",eval_equal "#equal_") |
176 Calc ("op =",eval_equal "#equal_") |
177 ]; |
177 ]; |
178 |
178 |
179 val Root_erls = |
179 val Root_erls = |
180 append_rls "Root_erls" Atools_erls |
180 append_rls "Root_erls" Atools_erls |
182 Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"), |
182 Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"), |
183 Calc ("Rings.inverse_class.divide",eval_cancel "#divide_e"), |
183 Calc ("Rings.inverse_class.divide",eval_cancel "#divide_e"), |
184 Calc ("Atools.pow" ,eval_binop "#power_"), |
184 Calc ("Atools.pow" ,eval_binop "#power_"), |
185 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
185 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
186 Calc ("Groups.minus_class.minus", eval_binop "#sub_"), |
186 Calc ("Groups.minus_class.minus", eval_binop "#sub_"), |
187 Calc ("op *", eval_binop "#mult_"), |
187 Calc ("Groups.times_class.times", eval_binop "#mult_"), |
188 Calc ("op =",eval_equal "#equal_") |
188 Calc ("op =",eval_equal "#equal_") |
189 ]; |
189 ]; |
190 |
190 |
191 ruleset' := overwritelthy @{theory} (!ruleset', |
191 ruleset' := overwritelthy @{theory} (!ruleset', |
192 [("Root_erls",Root_erls) (*FIXXXME:del with rls.rls'*) |
192 [("Root_erls",Root_erls) (*FIXXXME:del with rls.rls'*) |
250 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
250 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
251 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), |
251 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), |
252 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
252 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
253 |
253 |
254 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
254 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
255 Calc ("op *", eval_binop "#mult_"), |
255 Calc ("Groups.times_class.times", eval_binop "#mult_"), |
256 Calc ("Atools.pow", eval_binop "#power_") |
256 Calc ("Atools.pow", eval_binop "#power_") |
257 ], |
257 ], |
258 scr = Script ((term_of o the o (parse thy)) "empty_script") |
258 scr = Script ((term_of o the o (parse thy)) "empty_script") |
259 }:rls); |
259 }:rls); |
260 ruleset' := overwritelthy @{theory} (!ruleset', |
260 ruleset' := overwritelthy @{theory} (!ruleset', |
296 Thm ("add_0_left",num_str @{thm add_0_left}), |
296 Thm ("add_0_left",num_str @{thm add_0_left}), |
297 (*"0 + z = z"*) |
297 (*"0 + z = z"*) |
298 |
298 |
299 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
299 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
300 Calc ("Groups.minus_class.minus", eval_binop "#sub_"), |
300 Calc ("Groups.minus_class.minus", eval_binop "#sub_"), |
301 Calc ("op *", eval_binop "#mult_"), |
301 Calc ("Groups.times_class.times", eval_binop "#mult_"), |
302 Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"), |
302 Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"), |
303 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), |
303 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), |
304 Calc ("Atools.pow", eval_binop "#power_"), |
304 Calc ("Atools.pow", eval_binop "#power_"), |
305 |
305 |
306 Thm ("sym_realpow_twoI", |
306 Thm ("sym_realpow_twoI", |
321 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), |
321 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), |
322 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
322 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
323 |
323 |
324 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
324 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
325 Calc ("Groups.minus_class.minus", eval_binop "#sub_"), |
325 Calc ("Groups.minus_class.minus", eval_binop "#sub_"), |
326 Calc ("op *", eval_binop "#mult_"), |
326 Calc ("Groups.times_class.times", eval_binop "#mult_"), |
327 Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"), |
327 Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"), |
328 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), |
328 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), |
329 Calc ("Atools.pow", eval_binop "#power_") |
329 Calc ("Atools.pow", eval_binop "#power_") |
330 ], |
330 ], |
331 scr = Script ((term_of o the o (parse thy)) "empty_script") |
331 scr = Script ((term_of o the o (parse thy)) "empty_script") |