| changeset 5787 | 4e5c74b7cd9e |
| parent 5588 | a3ab526bb891 |
| child 7077 | 60b098bb8b8a |
--- 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