changeset 14390 | 55fe71faadda |
parent 14387 | e96d5c42c4b0 |
child 14430 | 5cb24165a2e1 |
--- a/src/HOL/Integ/nat_simprocs.ML Mon Feb 16 15:24:03 2004 +0100 +++ b/src/HOL/Integ/nat_simprocs.ML Tue Feb 17 10:41:59 2004 +0100 @@ -512,7 +512,7 @@ Suc_eq_number_of,eq_number_of_Suc, mult_Suc, mult_Suc_right, eq_number_of_0, eq_0_number_of, less_0_number_of, - nat_number_of, if_True, if_False]; + of_int_number_of_eq, of_nat_number_of_eq, nat_number_of, if_True, if_False]; val simprocs = [Nat_Numeral_Simprocs.combine_numerals]@ Nat_Numeral_Simprocs.cancel_numerals;