# HG changeset patch
# User paulson
# Date 1091024728 -7200
# Node ID 7912ace86f31d51e372721010d5f9c42c7a6daa7
# Parent  2ef899e4526d3697c436a046ce197d6e074f4177
fixed precedences

diff -r 2ef899e4526d -r 7912ace86f31 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Wed Jul 28 10:49:29 2004 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Wed Jul 28 16:25:28 2004 +0200
@@ -35,11 +35,11 @@
 
   (* differentiation: D is derivative of function f at x *)
   deriv:: "[real=>real,real,real] => bool"
-			    ("(DERIV (_)/ (_)/ :> (_))" [0, 0, 60] 60)
+			    ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
   "DERIV f x :> D == ((%h. (f(x + h) + -f x)/h) -- 0 --> D)"
 
   nsderiv :: "[real=>real,real,real] => bool"
-			    ("(NSDERIV (_)/ (_)/ :> (_))" [0, 0, 60] 60)
+			    ("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 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)"