src/HOL/Hyperreal/Lim.thy
changeset 15079 2ef899e4526d
parent 15077 89840837108e
child 15080 7912ace86f31
     1.1 --- a/src/HOL/Hyperreal/Lim.thy	Tue Jul 27 15:39:59 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/Lim.thy	Wed Jul 28 10:49:29 2004 +0200
     1.3 @@ -35,11 +35,11 @@
     1.4  
     1.5    (* differentiation: D is derivative of function f at x *)
     1.6    deriv:: "[real=>real,real,real] => bool"
     1.7 -			    ("(DERIV (_)/ (_)/ :> (_))" [60, 60, 60] 60)
     1.8 +			    ("(DERIV (_)/ (_)/ :> (_))" [0, 0, 60] 60)
     1.9    "DERIV f x :> D == ((%h. (f(x + h) + -f x)/h) -- 0 --> D)"
    1.10  
    1.11    nsderiv :: "[real=>real,real,real] => bool"
    1.12 -			    ("(NSDERIV (_)/ (_)/ :> (_))" [60, 60, 60] 60)
    1.13 +			    ("(NSDERIV (_)/ (_)/ :> (_))" [0, 0, 60] 60)
    1.14    "NSDERIV f x :> D == (\<forall>h \<in> Infinitesimal - {0}.
    1.15  			(( *f* f)(hypreal_of_real x + h) +
    1.16  			 - hypreal_of_real (f x))/h @= hypreal_of_real D)"