src/HOL/Num.thy

--- a/src/HOL/Num.thy	Mon Apr 02 14:09:27 2012 +0200
+++ b/src/HOL/Num.thy	Mon Apr 02 16:06:24 2012 +0200
@@ -865,8 +865,11 @@
   Natural numbers
 *}
 
+lemma Suc_1 [simp]: "Suc 1 = 2"
+  unfolding Suc_eq_plus1 by (rule one_add_one)
+
 lemma Suc_numeral [simp]: "Suc (numeral n) = numeral (n + One)"
-  unfolding numeral_plus_one [symmetric] by simp
+  unfolding Suc_eq_plus1 by (rule numeral_plus_one)
 
 definition pred_numeral :: "num \<Rightarrow> nat"
   where [code del]: "pred_numeral k = numeral k - 1"