src/HOL/Nat_Numeral.thy

--- a/src/HOL/Nat_Numeral.thy	Fri Mar 30 08:10:28 2012 +0200
+++ b/src/HOL/Nat_Numeral.thy	Fri Mar 30 08:11:52 2012 +0200
@@ -31,12 +31,6 @@
 
 subsubsection{*Arith *}
 
-lemma Suc_eq_plus1: "Suc n = n + 1"
-  unfolding One_nat_def by simp
-
-lemma Suc_eq_plus1_left: "Suc n = 1 + n"
-  unfolding One_nat_def by simp
-
 (* These two can be useful when m = numeral... *)
 
 lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"