remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int

--- a/src/HOL/IntDef.thy	Wed Jun 20 17:02:57 2007 +0200
+++ b/src/HOL/IntDef.thy	Wed Jun 20 17:28:55 2007 +0200
@@ -554,7 +554,8 @@
 qed
 
 lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
-by (cases z rule: eq_Abs_Integ, simp add: nat le of_int Zero_int_def)
+by (cases z rule: eq_Abs_Integ)
+   (simp add: nat le of_int Zero_int_def of_nat_diff)
 
 
 subsection{*The Set of Integers*}

--- a/src/HOL/Library/EfficientNat.thy	Wed Jun 20 17:02:57 2007 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Wed Jun 20 17:28:55 2007 +0200
@@ -105,7 +105,7 @@
 lemma [code func, code inline]: "m + n = nat_of_int (int' m + int' n)"
   by (simp add: eq_nat_of_int int'_add)
 lemma [code, code inline]: "m - n = nat (int' m - int' n)"
-  by (simp add: int'_def nat_eq_iff2)
+  by (simp add: int'_def nat_eq_iff2 of_nat_diff)
 lemma [code]: "m * n = nat (int' m * int' n)"
   unfolding int'_def
   by (simp add: of_nat_mult [symmetric] del: of_nat_mult)

--- a/src/HOL/Library/Parity.thy	Wed Jun 20 17:02:57 2007 +0200
+++ b/src/HOL/Library/Parity.thy	Wed Jun 20 17:28:55 2007 +0200
@@ -143,9 +143,9 @@
 
 lemma even_nat_difference:
     "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))"
-  apply (auto simp add: even_nat_def)
-  apply (case_tac "x < y", auto)
-  apply (case_tac "x < y", auto)
+  apply (auto simp add: even_nat_def zdiff_int [symmetric])
+  apply (case_tac "x < y", auto simp add: zdiff_int [symmetric])
+  apply (case_tac "x < y", auto simp add: zdiff_int [symmetric])
   done
 
 lemma even_nat_Suc: "even (Suc x) = odd x"

--- a/src/HOL/Nat.thy	Wed Jun 20 17:02:57 2007 +0200
+++ b/src/HOL/Nat.thy	Wed Jun 20 17:28:55 2007 +0200
@@ -1372,7 +1372,7 @@
 lemma inj_of_nat: "inj (of_nat :: nat \<Rightarrow> 'a::semiring_char_0)"
   by (simp add: inj_on_def)
 
-lemma of_nat_diff [simp]:
+lemma of_nat_diff:
     "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring_1)"
   by (simp del: of_nat_add
     add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)

--- a/src/HOL/Presburger.thy	Wed Jun 20 17:02:57 2007 +0200
+++ b/src/HOL/Presburger.thy	Wed Jun 20 17:28:55 2007 +0200
@@ -389,7 +389,7 @@
 
 lemma zdiff_int_split: "P (int (x - y)) =
   ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
-  by (case_tac "y \<le> x", simp_all)
+  by (case_tac "y \<le> x", simp_all add: zdiff_int)
 
 lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" by simp
 lemma number_of2: "(0::int) <= Numeral0" by simp

--- a/src/HOL/Real/RealDef.thy	Wed Jun 20 17:02:57 2007 +0200
+++ b/src/HOL/Real/RealDef.thy	Wed Jun 20 17:28:55 2007 +0200
@@ -739,7 +739,7 @@
 by (simp add: real_of_nat_def)
 
 lemma real_of_nat_diff: "n \<le> m ==> real (m - n) = real (m::nat) - real n"
-by (simp add: add: real_of_nat_def) 
+by (simp add: add: real_of_nat_def of_nat_diff)
 
 lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)"
 by (simp add: add: real_of_nat_def)