src/HOL/Integ/int_arith1.ML
changeset 16473 b24c820a0b85
parent 16423 24abe4c0e4b4
child 16973 b2a894562b8f
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Mon Jun 20 11:45:40 2005 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Mon Jun 20 15:54:22 2005 +0200
     1.3 @@ -504,9 +504,7 @@
     1.4       minus_mult_left RS sym, minus_mult_right RS sym,
     1.5       minus_add_distrib, minus_minus, mult_assoc,
     1.6       of_nat_0, of_nat_1, of_nat_Suc, of_nat_add, of_nat_mult,
     1.7 -     of_int_0, of_int_1, of_int_add, of_int_mult, int_eq_of_nat,
     1.8 -     zero_neq_one, zero_less_one, zero_le_one, 
     1.9 -     zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero];
    1.10 +     of_int_0, of_int_1, of_int_add, of_int_mult, int_eq_of_nat];
    1.11  
    1.12  val simprocs = [assoc_fold_simproc, Int_Numeral_Simprocs.combine_numerals]@
    1.13                 Int_Numeral_Simprocs.cancel_numerals;