# HG changeset patch
# User huffman
# Date 1333375584 -7200
# Node ID e705ef5ffe958ae8ac088b62c9e9fbc214c167af
# Parent  8b63aaec0a0e5d4813bc7bb7676849880a6b45dd
add lemma Suc_1

diff -r 8b63aaec0a0e -r e705ef5ffe95 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"