src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Wed Jun 14 12:14:13 2006 +0200
+++ b/src/HOL/Nat.thy	Wed Jun 14 12:14:42 2006 +0200
@@ -601,7 +601,8 @@
 lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
   by (induct m) simp_all
 
-lemma [code]: "Suc m + n = m + Suc n" by simp
+lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
+  by simp
 
 
 text {* Associative law for addition *}