Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed precedences
authorpaulson
Wed, 28 Jul 2004 16:25:28 +0200
changeset 15080 7912ace86f31
parent 15079 2ef899e4526d
child 15081 32402f5624d1
fixed precedences
src/HOL/Hyperreal/Lim.thy file | annotate | diff | comparison | revisions 
--- 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)"
isabelle