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 read_instantiate_sg (sign_of(the_context())) |
577 mult_Suc, mult_Suc_right, |
578 [("m","number_of ?v")] mult_Suc, |
|
579 read_instantiate_sg (sign_of(the_context())) |
|
580 [("m","number_of ?v")] mult_Suc_right, |
|
581 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, |
582 nat_number_of, Let_number_of, if_True, if_False]; |
579 nat_number_of, Let_number_of, if_True, if_False]; |
583 |
580 |
584 val simprocs = [Nat_Times_Assoc.conv, |
581 val simprocs = [Nat_Times_Assoc.conv, |
585 Nat_Numeral_Simprocs.combine_numerals]@ |
582 Nat_Numeral_Simprocs.combine_numerals]@ |