--- a/src/HOL/Tools/numeral_simprocs.ML Sun Feb 07 18:04:48 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Sun Feb 07 19:31:55 2010 +0100
@@ -181,9 +181,8 @@
(*To let us treat division as multiplication*)
val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}];
-(*push the unary minus down: - x * y = x * - y *)
-val minus_mult_eq_1_to_2 =
- [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> Drule.standard;
+(*push the unary minus down*)
+val minus_mult_eq_1_to_2 = @{lemma "- (a::'a::ring) * b = a * - b" by simp};
(*to extract again any uncancelled minuses*)
val minus_from_mult_simps =
--- a/src/ZF/int_arith.ML Sun Feb 07 18:04:48 2010 +0100
+++ b/src/ZF/int_arith.ML Sun Feb 07 19:31:55 2010 +0100
@@ -110,9 +110,8 @@
(*To let us treat subtraction as addition*)
val diff_simps = [@{thm zdiff_def}, @{thm zminus_zadd_distrib}, @{thm zminus_zminus}];
-(*push the unary minus down: - x * y = x * - y *)
-val int_minus_mult_eq_1_to_2 =
- [@{thm zmult_zminus}, @{thm zmult_zminus_right} RS sym] MRS trans |> Drule.standard;
+(*push the unary minus down*)
+val int_minus_mult_eq_1_to_2 = @{lemma "$- w $* z = w $* $- z" by simp};
(*to extract again any uncancelled minuses*)
val int_minus_from_mult_simps =