equal
deleted
inserted
replaced
44 (b * a) = (a * b)" and |
44 (b * a) = (a * b)" and |
45 tausche_vor_mal: "[| b is_atom; a kleiner b |] ==> |
45 tausche_vor_mal: "[| b is_atom; a kleiner b |] ==> |
46 (-b * a) = (-a * b)" and |
46 (-b * a) = (-a * b)" and |
47 tausche_mal_mal: "[| c is_atom; b kleiner c |] ==> |
47 tausche_mal_mal: "[| c is_atom; b kleiner c |] ==> |
48 (x * c * b) = (x * b * c)" and |
48 (x * c * b) = (x * b * c)" and |
49 x_quadrat: "(x * a) * a = x * a ^^^ 2" and |
49 x_quadrat: "(x * a) * a = x * a \<up> 2" and |
50 |
50 |
51 |
51 |
52 subtrahiere: "[| l is_const; m is_const |] ==> |
52 subtrahiere: "[| l is_const; m is_const |] ==> |
53 m * v - l * v = (m - l) * v" and |
53 m * v - l * v = (m - l) * v" and |
54 subtrahiere_von_1: "[| l is_const |] ==> |
54 subtrahiere_von_1: "[| l is_const |] ==> |
352 Rule.Thm ("tausche_vor_mal",ThmC.numerals_to_Free @{thm tausche_vor_mal}), |
352 Rule.Thm ("tausche_vor_mal",ThmC.numerals_to_Free @{thm tausche_vor_mal}), |
353 (*"[| b is_atom; a kleiner b |] ==> (-b * a) = (-a * b)"*) |
353 (*"[| b is_atom; a kleiner b |] ==> (-b * a) = (-a * b)"*) |
354 Rule.Thm ("tausche_mal_mal",ThmC.numerals_to_Free @{thm tausche_mal_mal}), |
354 Rule.Thm ("tausche_mal_mal",ThmC.numerals_to_Free @{thm tausche_mal_mal}), |
355 (*"[| c is_atom; b kleiner c |] ==> (a * c * b) = (a * b *c)"*) |
355 (*"[| c is_atom; b kleiner c |] ==> (a * c * b) = (a * b *c)"*) |
356 Rule.Thm ("x_quadrat",ThmC.numerals_to_Free @{thm x_quadrat}) |
356 Rule.Thm ("x_quadrat",ThmC.numerals_to_Free @{thm x_quadrat}) |
357 (*"(x * a) * a = x * a ^^^ 2"*) |
357 (*"(x * a) * a = x * a \<up> 2"*) |
358 |
358 |
359 (*Rule.Thm ("",ThmC.numerals_to_Free @{}), |
359 (*Rule.Thm ("",ThmC.numerals_to_Free @{}), |
360 (*""*)*) |
360 (*""*)*) |
361 ], scr = Rule.Empty_Prog}; |
361 ], scr = Rule.Empty_Prog}; |
362 |
362 |