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