# HG changeset patch
# User bulwahn
# Date 1327742566 -3600
# Node ID a49c89df7c924f1299b91448bdb5ae0f5980dc78
# Parent  b159ca4e268bda94c9e3584cbd14fc99ec84d0a2
moving declarations back to the section they seem to belong to (cf. afffe1f72143)

diff -r b159ca4e268b -r a49c89df7c92 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat Jan 28 06:13:03 2012 +0100
+++ b/src/HOL/Nat.thy	Sat Jan 28 10:22:46 2012 +0100
@@ -1616,6 +1616,17 @@
 lemma Suc_diff_Suc: "n < m \<Longrightarrow> Suc (m - Suc n) = m - n"
 by simp
 
+(*The others are
+      i - j - k = i - (j + k),
+      k \<le> j ==> j - k + i = j + i - k,
+      k \<le> j ==> i + (j - k) = i + j - k *)
+lemmas add_diff_assoc = diff_add_assoc [symmetric]
+lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
+declare diff_diff_left [simp]  add_diff_assoc [simp] add_diff_assoc2[simp]
+
+text{*At present we prove no analogue of @{text not_less_Least} or @{text
+Least_Suc}, since there appears to be no need.*}
+
 text{*Lemmas for ex/Factorization*}
 
 lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
@@ -1669,17 +1680,6 @@
 lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
   using inc_induct[of 0 k P] by blast
 
-(*The others are
-      i - j - k = i - (j + k),
-      k \<le> j ==> j - k + i = j + i - k,
-      k \<le> j ==> i + (j - k) = i + j - k *)
-lemmas add_diff_assoc = diff_add_assoc [symmetric]
-lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
-declare diff_diff_left [simp]  add_diff_assoc [simp] add_diff_assoc2[simp]
-
-text{*At present we prove no analogue of @{text not_less_Least} or @{text
-Least_Suc}, since there appears to be no need.*}
-
 
 subsection {* The divides relation on @{typ nat} *}