392 val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @ |
392 val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @ |
393 [int_0, zadd_0, zadd_0_right, zdiff_def, |
393 [int_0, zadd_0, zadd_0_right, zdiff_def, |
394 zadd_zminus_inverse, zadd_zminus_inverse2, |
394 zadd_zminus_inverse, zadd_zminus_inverse2, |
395 zmult_0, zmult_0_right, |
395 zmult_0, zmult_0_right, |
396 zmult_1, zmult_1_right, |
396 zmult_1, zmult_1_right, |
397 zmult_minus1, zmult_minus1_right]; |
397 zmult_minus1, zmult_minus1_right, |
|
398 zminus_zadd_distrib, zminus_zminus]; |
398 |
399 |
399 val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@ |
400 val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@ |
400 Int_Numeral_Simprocs.cancel_numerals; |
401 Int_Numeral_Simprocs.cancel_numerals; |
401 |
402 |
402 val add_mono_thms = |
403 val add_mono_thms = |