--- a/src/HOL/Hyperreal/Lim.thy Tue Jul 27 15:39:59 2004 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Wed Jul 28 10:49:29 2004 +0200
@@ -35,11 +35,11 @@
(* differentiation: D is derivative of function f at x *)
deriv:: "[real=>real,real,real] => bool"
- ("(DERIV (_)/ (_)/ :> (_))" [60, 60, 60] 60)
+ ("(DERIV (_)/ (_)/ :> (_))" [0, 0, 60] 60)
"DERIV f x :> D == ((%h. (f(x + h) + -f x)/h) -- 0 --> D)"
nsderiv :: "[real=>real,real,real] => bool"
- ("(NSDERIV (_)/ (_)/ :> (_))" [60, 60, 60] 60)
+ ("(NSDERIV (_)/ (_)/ :> (_))" [0, 0, 60] 60)
"NSDERIV f x :> D == (\<forall>h \<in> Infinitesimal - {0}.
(( *f* f)(hypreal_of_real x + h) +
- hypreal_of_real (f x))/h @= hypreal_of_real D)"