src/HOL/Nat.thy

--- 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)