diff -r fb0a80aef0be -r 5b57f995a179 src/HOL/NatArith.thy
--- a/src/HOL/NatArith.thy	Tue Aug 16 15:36:28 2005 +0200
+++ b/src/HOL/NatArith.thy	Tue Aug 16 18:53:11 2005 +0200
@@ -123,9 +123,9 @@
       i - j - k = i - (j + k),
       k \<le> j ==> j - k + i = j + i - k,
       k \<le> j ==> i + (j - k) = i + j - k *)
-declare diff_diff_left [simp] 
-        diff_add_assoc [symmetric, simp]
-        diff_add_assoc2[symmetric, simp]
+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.*}
@@ -206,16 +206,20 @@
 by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
 
 text{*Special cases where either operand is zero*}
-declare of_nat_less_iff [of 0, simplified, simp]
-declare of_nat_less_iff [of _ 0, simplified, simp]
+lemmas of_nat_0_less_iff = of_nat_less_iff [of 0, simplified]
+lemmas of_nat_less_0_iff = of_nat_less_iff [of _ 0, simplified]
+declare of_nat_0_less_iff [simp]
+declare of_nat_less_0_iff [simp]
 
 lemma of_nat_le_iff [simp]:
      "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
 by (simp add: linorder_not_less [symmetric])
 
 text{*Special cases where either operand is zero*}
-declare of_nat_le_iff [of 0, simplified, simp]
-declare of_nat_le_iff [of _ 0, simplified, simp]
+lemmas of_nat_0_le_iff = of_nat_le_iff [of 0, simplified]
+lemmas of_nat_le_0_iff = of_nat_le_iff [of _ 0, simplified]
+declare of_nat_0_le_iff [simp]
+declare of_nat_le_0_iff [simp]
 
 text{*The ordering on the @{text comm_semiring_1_cancel} is necessary
 to exclude the possibility of a finite field, which indeed wraps back to
@@ -225,8 +229,10 @@
 by (simp add: order_eq_iff)
 
 text{*Special cases where either operand is zero*}
-declare of_nat_eq_iff [of 0, simplified, simp]
-declare of_nat_eq_iff [of _ 0, simplified, simp]
+lemmas of_nat_0_eq_iff = of_nat_eq_iff [of 0, simplified]
+lemmas of_nat_eq_0_iff = of_nat_eq_iff [of _ 0, simplified]
+declare of_nat_0_eq_iff [simp]
+declare of_nat_eq_0_iff [simp]
 
 lemma of_nat_diff [simp]:
      "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::comm_ring_1)"