572 [add_nat_number_of, diff_nat_number_of, mult_nat_number_of, |
572 [add_nat_number_of, diff_nat_number_of, mult_nat_number_of, |
573 eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less, |
573 eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less, |
574 le_Suc_number_of,le_number_of_Suc, |
574 le_Suc_number_of,le_number_of_Suc, |
575 less_Suc_number_of,less_number_of_Suc, |
575 less_Suc_number_of,less_number_of_Suc, |
576 Suc_eq_number_of,eq_number_of_Suc, |
576 Suc_eq_number_of,eq_number_of_Suc, |
577 mult_Suc, mult_Suc_right, |
577 mult_0, mult_0_right, mult_Suc, mult_Suc_right, |
578 eq_number_of_0, eq_0_number_of, less_0_number_of, |
578 eq_number_of_0, eq_0_number_of, less_0_number_of, |
579 nat_number_of, Let_number_of, if_True, if_False]; |
579 nat_number_of, Let_number_of, if_True, if_False]; |
580 |
580 |
581 val simprocs = [Nat_Times_Assoc.conv, |
581 val simprocs = [Nat_Times_Assoc.conv, |
582 Nat_Numeral_Simprocs.combine_numerals]@ |
582 Nat_Numeral_Simprocs.combine_numerals]@ |