510 le_Suc_number_of,le_number_of_Suc, |
510 le_Suc_number_of,le_number_of_Suc, |
511 less_Suc_number_of,less_number_of_Suc, |
511 less_Suc_number_of,less_number_of_Suc, |
512 Suc_eq_number_of,eq_number_of_Suc, |
512 Suc_eq_number_of,eq_number_of_Suc, |
513 mult_Suc, mult_Suc_right, |
513 mult_Suc, mult_Suc_right, |
514 eq_number_of_0, eq_0_number_of, less_0_number_of, |
514 eq_number_of_0, eq_0_number_of, less_0_number_of, |
515 nat_number_of, if_True, if_False]; |
515 of_int_number_of_eq, of_nat_number_of_eq, nat_number_of, if_True, if_False]; |
516 |
516 |
517 val simprocs = [Nat_Numeral_Simprocs.combine_numerals]@ |
517 val simprocs = [Nat_Numeral_Simprocs.combine_numerals]@ |
518 Nat_Numeral_Simprocs.cancel_numerals; |
518 Nat_Numeral_Simprocs.cancel_numerals; |
519 |
519 |
520 in |
520 in |