# HG changeset patch
# User nipkow
# Date 989581755 -7200
# Node ID 38a69e5d79faecbd3f5e7a907847418f034f01d8
# Parent  66925f23ac7feec05b713cd8cb761d154c281966
added mult_Suc laws to lin.arith.simpset.
removed Suc n = n + #1 added earlier - #1::nat is not expected by Larry's
simprocs.

diff -r 66925f23ac7f -r 38a69e5d79fa src/HOL/Integ/NatSimprocs.ML
--- a/src/HOL/Integ/NatSimprocs.ML	Thu May 10 17:28:40 2001 +0200
+++ b/src/HOL/Integ/NatSimprocs.ML	Fri May 11 13:49:15 2001 +0200
@@ -30,8 +30,6 @@
 by (asm_full_simp_tac
     (simpset_of Int.thy addsimps [diff_nat_number_of, less_0_number_of RS sym,
                                   neg_number_of_bin_pred_iff_0]) 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset_of Int.thy) 1);
 qed "Suc_diff_number_of";
 
 (* now redundant because of the inverse_fold simproc
diff -r 66925f23ac7f -r 38a69e5d79fa src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Thu May 10 17:28:40 2001 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML	Fri May 11 13:49:15 2001 +0200
@@ -571,10 +571,13 @@
 val add_rules =
   [add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
    eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less,
-   (*le_Suc_number_of,le_number_of_Suc,
+   le_Suc_number_of,le_number_of_Suc,
    less_Suc_number_of,less_number_of_Suc,
-   Suc_eq_number_of,eq_number_of_Suc*)
-   Suc_eq_add_numeral_1,
+   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,
    eq_number_of_0, eq_0_number_of, less_0_number_of,
    nat_number_of, Let_number_of, if_True, if_False];