src/ZF/int_arith.ML
changeset 32957 675c0c7e6a37
parent 32155 e2bf2f73b0c8
child 35020 862a20ffa8e2
     1.1 --- a/src/ZF/int_arith.ML	Fri Oct 16 10:55:07 2009 +0200
     1.2 +++ b/src/ZF/int_arith.ML	Sat Oct 17 00:52:37 2009 +0200
     1.3 @@ -112,7 +112,7 @@
     1.4  
     1.5  (*push the unary minus down: - x * y = x * - y *)
     1.6  val int_minus_mult_eq_1_to_2 =
     1.7 -    [@{thm zmult_zminus}, @{thm zmult_zminus_right} RS sym] MRS trans |> standard;
     1.8 +    [@{thm zmult_zminus}, @{thm zmult_zminus_right} RS sym] MRS trans |> Drule.standard;
     1.9  
    1.10  (*to extract again any uncancelled minuses*)
    1.11  val int_minus_from_mult_simps =