# HG changeset patch
# User wenzelm
# Date 1265567515 -3600
# Node ID 862a20ffa8e2dd23c973fe364dbb5be9b8251227
# Parent  1ec0a3ff229e4d835d19d4fcd6b2ac2bb077dd44
prefer explicit @{lemma} over adhoc forward reasoning;

diff -r 1ec0a3ff229e -r 862a20ffa8e2 src/HOL/Tools/numeral_simprocs.ML
--- 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 =
diff -r 1ec0a3ff229e -r 862a20ffa8e2 src/ZF/int_arith.ML
--- 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 =