src/HOL/Integ/int_arith1.ML
changeset 11713 883d559b0b8c
parent 11704 3c50a2cd6f00
child 11868 56db9f3a6b3e
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Mon Oct 08 14:30:28 2001 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Mon Oct 08 15:23:20 2001 +0200
     1.3 @@ -410,7 +410,7 @@
     1.4  		 zmult_1, zmult_1_right, 
     1.5  		 zmult_minus1, zmult_minus1_right,
     1.6  		 zminus_zadd_distrib, zminus_zminus, zmult_assoc,
     1.7 -                 Zero_int_def, int_0, zadd_int RS sym, int_Suc];
     1.8 +                 Zero_int_def, One_int_def, int_0, int_1, zadd_int RS sym, int_Suc];
     1.9  
    1.10  val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
    1.11                 Int_Numeral_Simprocs.cancel_numerals;