diff -r 2cc3352f6c3c -r 0b5a400c7595 src/HOL/Hyperreal/HDeriv.thy
--- 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)