--- a/src/HOL/Hyperreal/HDeriv.thy Fri Jun 15 09:10:06 2007 +0200
+++ b/src/HOL/Hyperreal/HDeriv.thy Fri Jun 15 15:10:32 2007 +0200
@@ -338,7 +338,7 @@
text{*Differentiation of natural number powers*}
lemma NSDERIV_Id [simp]: "NSDERIV (%x. x) x :> 1"
-by (simp add: NSDERIV_NSLIM_iff NSLIM_def divide_self del: divide_self_if)
+by (simp add: NSDERIV_NSLIM_iff NSLIM_def del: divide_self_if)
lemma NSDERIV_cmult_Id [simp]: "NSDERIV (op * c) x :> c"
by (cut_tac c = c and x = x in NSDERIV_Id [THEN NSDERIV_cmult], simp)