# HG changeset patch
# User paulson
# Date 910006576 -3600
# Node ID 4e5c74b7cd9e17579a4a3f783371822c0ca61fe2
# Parent  9a2c90bdadfeb8c43f871e3f5abdf983bdf4f41c
increased precedence of unary minus from 80 to 100
requires a similar increase for %# and %%#

diff -r 9a2c90bdadfe -r 4e5c74b7cd9e src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Mon Nov 02 12:35:14 1998 +0100
+++ b/src/HOL/Real/RealDef.thy	Mon Nov 02 12:36:16 1998 +0100
@@ -33,13 +33,13 @@
 
 constdefs
 
-  real_preal :: preal => real              ("%#_" [80] 80)
+  real_preal :: preal => real              ("%#_" [100] 100)
   "%# m     == Abs_real(realrel^^{(m+@#($#1p),@#($#1p))})"
 
   rinv       :: real => real
   "rinv(R)   == (@S. R ~= 0r & S*R = 1r)"
 
-  real_nat :: nat => real                  ("%%# _" [80] 80) 
+  real_nat :: nat => real                  ("%%# _" [100] 100) 
   "%%# n      == %#(@#($#(*# n)))"
 
 defs