merged

--- a/src/HOL/Nat.thy	Wed Feb 25 11:49:05 2009 +0100
+++ b/src/HOL/Nat.thy	Wed Feb 25 07:14:33 2009 -0800
@@ -280,6 +280,9 @@
 lemma diff_add_0: "n - (n + m) = (0::nat)"
   by (induct n) simp_all
 
+lemma diff_Suc_1 [simp]: "Suc n - 1 = n"
+  unfolding One_nat_def by simp
+
 text {* Difference distributes over multiplication *}
 
 lemma diff_mult_distrib: "((m::nat) - n) * k = (m * k) - (n * k)"