src/HOL/Integ/int_arith1.ML
changeset 14390 55fe71faadda
parent 14387 e96d5c42c4b0
child 14474 00292f6f8d13
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Mon Feb 16 15:24:03 2004 +0100
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Tue Feb 17 10:41:59 2004 +0100
     1.3 @@ -476,7 +476,7 @@
     1.4  (* reduce contradictory <= to False *)
     1.5  val add_rules =
     1.6      simp_thms @ bin_arith_simps @ bin_rel_simps @ arith_special @
     1.7 -    [numeral_0_eq_0, numeral_1_eq_1,
     1.8 +    [neg_le_iff_le, numeral_0_eq_0, numeral_1_eq_1,
     1.9       minus_zero, diff_minus, left_minus, right_minus,
    1.10       mult_zero_left, mult_zero_right, mult_1, mult_1_right,
    1.11       minus_mult_left RS sym, minus_mult_right RS sym,