260 Thm ("subtrahiere_x_minus1_minus",num_str @{thm subtrahiere_x_minus1_minus}), |
260 Thm ("subtrahiere_x_minus1_minus",num_str @{thm subtrahiere_x_minus1_minus}), |
261 (*"[| l is_const |] ==> (x - v) - l * v = x + (-1 - l) * v"*) |
261 (*"[| l is_const |] ==> (x - v) - l * v = x + (-1 - l) * v"*) |
262 Thm ("subtrahiere_x_minus_minus1",num_str @{thm subtrahiere_x_minus_minus1}), |
262 Thm ("subtrahiere_x_minus_minus1",num_str @{thm subtrahiere_x_minus_minus1}), |
263 (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*) |
263 (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*) |
264 |
264 |
265 Calc ("op +", eval_binop "#add_"), |
265 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
266 Calc ("op -", eval_binop "#subtr_"), |
266 Calc ("Groups.minus_class.minus", eval_binop "#subtr_"), |
267 |
267 |
268 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen |
268 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen |
269 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *) |
269 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *) |
270 Thm ("real_mult_2_assoc_r",num_str @{thm real_mult_2_assoc_r}), |
270 Thm ("real_mult_2_assoc_r",num_str @{thm real_mult_2_assoc_r}), |
271 (*"(k + z1) + z1 = k + 2 * z1"*) |
271 (*"(k + z1) + z1 = k + 2 * z1"*) |
380 Rls_ verschoenere |
380 Rls_ verschoenere |
381 ]; |
381 ]; |
382 val rechnen = |
382 val rechnen = |
383 append_rls "rechnen" e_rls |
383 append_rls "rechnen" e_rls |
384 [Calc ("op *", eval_binop "#mult_"), |
384 [Calc ("op *", eval_binop "#mult_"), |
385 Calc ("op +", eval_binop "#add_"), |
385 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
386 Calc ("op -", eval_binop "#subtr_") |
386 Calc ("Groups.minus_class.minus", eval_binop "#subtr_") |
387 ]; |
387 ]; |
388 |
388 |
389 ruleset' := |
389 ruleset' := |
390 overwritelthy @{theory} (!ruleset', |
390 overwritelthy @{theory} (!ruleset', |
391 [("ordne_alphabetisch", prep_rls ordne_alphabetisch), |
391 [("ordne_alphabetisch", prep_rls ordne_alphabetisch), |