*** empty log message ***
authornipkow
Thu Dec 21 16:52:10 2000 +0100 (2000-12-21)
changeset 107198666477dd9a2
parent 10718 c058f78c3544
child 10720 1ce5a189f672
*** empty log message ***
src/HOL/Integ/int_arith1.ML
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Thu Dec 21 16:19:39 2000 +0100
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Thu Dec 21 16:52:10 2000 +0100
     1.3 @@ -409,8 +409,8 @@
     1.4  		 zmult_0, zmult_0_right, 
     1.5  		 zmult_1, zmult_1_right, 
     1.6  		 zmult_minus1, zmult_minus1_right,
     1.7 -		 zminus_zadd_distrib, zminus_zminus,
     1.8 -                 int_0, zadd_int RS sym, int_Suc];
     1.9 +		 zminus_zadd_distrib, zminus_zminus, zmult_assoc,
    1.10 +                 IntDef.Zero_def, int_0, zadd_int RS sym, int_Suc];
    1.11  
    1.12  val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
    1.13                 Int_Numeral_Simprocs.cancel_numerals;