# HG changeset patch
# User huffman
# Date 1333087912 -7200
# Node ID 9a91b163bb719d2aa654d6a53d7fe0fb0168784f
# Parent  9368aa81451804e09ad72c3cdd13e5cc359cf2d0
move lemmas from Nat_Numeral.thy to Nat.thy

diff -r 9368aa814518 -r 9a91b163bb71 src/HOL/Nat.thy
--- 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 *}
 
diff -r 9368aa814518 -r 9a91b163bb71 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))"