adapted to new times_divide_eq simp situation
authorhaftmann
Fri Apr 23 16:17:25 2010 +0200 (2010-04-23)
changeset 36310e3d3b14b13cd
parent 36309 4da07afb065b
child 36311 ed3a87a7f977
adapted to new times_divide_eq simp situation
src/HOL/NSA/HDeriv.thy
     1.1 --- a/src/HOL/NSA/HDeriv.thy	Fri Apr 23 16:17:25 2010 +0200
     1.2 +++ b/src/HOL/NSA/HDeriv.thy	Fri Apr 23 16:17:25 2010 +0200
     1.3 @@ -204,7 +204,7 @@
     1.4  apply (simp (no_asm) add: add_divide_distrib diff_divide_distrib)
     1.5  apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
     1.6  apply (auto simp add: times_divide_eq_right [symmetric]
     1.7 -            simp del: times_divide_eq)
     1.8 +            simp del: times_divide_eq_right times_divide_eq_left)
     1.9  apply (drule_tac D = Db in lemma_nsderiv2, assumption+)
    1.10  apply (drule_tac
    1.11       approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]])