src/HOL/Tools/numeral_simprocs.ML
changeset 35020 862a20ffa8e2
parent 34974 18b41bba42b5
child 35030 f2f1e50bf65d
     1.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Sun Feb 07 18:04:48 2010 +0100
     1.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Sun Feb 07 19:31:55 2010 +0100
     1.3 @@ -181,9 +181,8 @@
     1.4  (*To let us treat division as multiplication*)
     1.5  val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}];
     1.6  
     1.7 -(*push the unary minus down: - x * y = x * - y *)
     1.8 -val minus_mult_eq_1_to_2 =
     1.9 -    [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> Drule.standard;
    1.10 +(*push the unary minus down*)
    1.11 +val minus_mult_eq_1_to_2 = @{lemma "- (a::'a::ring) * b = a * - b" by simp};
    1.12  
    1.13  (*to extract again any uncancelled minuses*)
    1.14  val minus_from_mult_simps =