diff -r ad1ffcc90162 -r e96d5c42c4b0 src/HOL/Hyperreal/Lim.ML
--- a/src/HOL/Hyperreal/Lim.ML	Sat Feb 14 02:06:12 2004 +0100
+++ b/src/HOL/Hyperreal/Lim.ML	Sun Feb 15 10:46:37 2004 +0100
@@ -1405,7 +1405,7 @@
 Goal "(\\<forall>z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l \
 \     ==> NSDERIV f x :> l";
 by (auto_tac (claset(), 
-              simpset() delsimprocs real_cancel_factor
+              simpset() delsimprocs field_cancel_factor
                         addsimps [NSDERIV_iff2]));
 by (auto_tac (claset(),
               simpset() addsimps [hypreal_mult_assoc]));
@@ -1877,9 +1877,25 @@
               addsplits [split_if_asm]) 1); 
 qed "DERIV_left_inc";
 
-Goalw [deriv_def,LIM_def] 
+val prems = goalw (the_context()) [deriv_def,LIM_def]
     "[| DERIV f x :> l;  l < 0 |] ==> \
 \      \\<exists>d. 0 < d & (\\<forall>h. 0 < h & h < d --> f(x) < f(x - h))";
+by (cut_facts_tac prems 1);  (*needed because arith removes the assumption l<0*)
+by (dres_inst_tac [("x","-l")] spec 1 THEN Auto_tac);
+by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac);
+by (dres_inst_tac [("x","-h")] spec 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [real_abs_def, inverse_eq_divide, 
+                         pos_less_divide_eq,
+                         symmetric real_diff_def]
+               addsplits [split_if_asm]) 1);
+by (subgoal_tac "0 < (f (x - h) - f x)/h" 1);
+by (asm_full_simp_tac (simpset() addsimps [pos_less_divide_eq]) 1); 
+by (cut_facts_tac prems 1);
+by (arith_tac 1);
+qed "DERIV_left_dec";
+
+(*????previous proof, revealing arith problem:
 by (dres_inst_tac [("x","-l")] spec 1 THEN Auto_tac);
 by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac);
 by (subgoal_tac "l*h < 0" 1);
@@ -1896,6 +1912,7 @@
 by (asm_full_simp_tac
     (simpset() addsimps [pos_less_divide_eq]) 1); 
 qed "DERIV_left_dec";
+*)
 
 
 Goal "[| DERIV f x :> l; \