src/HOL/Integ/nat_simprocs.ML
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;