changeset 21210 | c17fd2df4e9e |
parent 20217 | 25b068a99d2b |
child 21404 | eb85850d3eb7 |
--- a/src/HOL/Real/RComplete.thy Tue Nov 07 11:47:56 2006 +0100 +++ b/src/HOL/Real/RComplete.thy Tue Nov 07 11:47:57 2006 +0100 @@ -438,11 +438,11 @@ ceiling :: "real => int" "ceiling r = - floor (- r)" -const_syntax (xsymbols) +notation (xsymbols) floor ("\<lfloor>_\<rfloor>") ceiling ("\<lceil>_\<rceil>") -const_syntax (HTML output) +notation (HTML output) floor ("\<lfloor>_\<rfloor>") ceiling ("\<lceil>_\<rceil>")