mult_Suc generally, not just for numerals.
authornipkow
Fri, 11 May 2001 15:57:42 +0200
changeset 11297 2d73013f3a41
parent 11296 38a69e5d79fa
child 11298 acd83fa66e92
mult_Suc generally, not just for numerals.
src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Fri May 11 13:49:15 2001 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML	Fri May 11 15:57:42 2001 +0200
@@ -574,10 +574,7 @@
    le_Suc_number_of,le_number_of_Suc,
    less_Suc_number_of,less_number_of_Suc,
    Suc_eq_number_of,eq_number_of_Suc,
-   read_instantiate_sg (sign_of(the_context()))
-      [("m","number_of ?v")] mult_Suc,
-   read_instantiate_sg (sign_of(the_context()))
-      [("m","number_of ?v")] mult_Suc_right,
+   mult_Suc, mult_Suc_right,
    eq_number_of_0, eq_0_number_of, less_0_number_of,
    nat_number_of, Let_number_of, if_True, if_False];