--- a/src/HOL/Nat.thy Fri Mar 30 08:10:28 2012 +0200
+++ b/src/HOL/Nat.thy Fri Mar 30 08:11:52 2012 +0200
@@ -252,6 +252,12 @@
apply (simp add:o_def)
done
+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
+
subsubsection {* Difference *}
--- 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))"