# HG changeset patch
# User haftmann
# Date 1272032245 -7200
# Node ID e3d3b14b13cd955eb0c2b136218693555d9dea82
# Parent  4da07afb065bfdcdc6d526206f1f98f6eb127fe1
adapted to new times_divide_eq simp situation

diff -r 4da07afb065b -r e3d3b14b13cd src/HOL/NSA/HDeriv.thy
--- a/src/HOL/NSA/HDeriv.thy	Fri Apr 23 16:17:25 2010 +0200
+++ b/src/HOL/NSA/HDeriv.thy	Fri Apr 23 16:17:25 2010 +0200
@@ -204,7 +204,7 @@
 apply (simp (no_asm) add: add_divide_distrib diff_divide_distrib)
 apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
 apply (auto simp add: times_divide_eq_right [symmetric]
-            simp del: times_divide_eq)
+            simp del: times_divide_eq_right times_divide_eq_left)
 apply (drule_tac D = Db in lemma_nsderiv2, assumption+)
 apply (drule_tac
      approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]])