--- a/src/HOL/Integ/NatSimprocs.ML Wed Apr 18 22:09:45 2001 +0200
+++ b/src/HOL/Integ/NatSimprocs.ML Thu Apr 19 13:36:07 2001 +0200
@@ -30,6 +30,8 @@
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
--- a/src/HOL/Integ/nat_simprocs.ML Wed Apr 18 22:09:45 2001 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML Thu Apr 19 13:36:07 2001 +0200
@@ -571,9 +571,10 @@
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_number_of,eq_number_of_Suc*)
+ Suc_eq_add_numeral_1,
eq_number_of_0, eq_0_number_of, less_0_number_of,
nat_number_of, Let_number_of, if_True, if_False];