src/HOL/Real/RComplete.thy
changeset 21210 c17fd2df4e9e
parent 20217 25b068a99d2b
child 21404 eb85850d3eb7
     1.1 --- a/src/HOL/Real/RComplete.thy	Tue Nov 07 11:47:56 2006 +0100
     1.2 +++ b/src/HOL/Real/RComplete.thy	Tue Nov 07 11:47:57 2006 +0100
     1.3 @@ -438,11 +438,11 @@
     1.4    ceiling :: "real => int"
     1.5    "ceiling r = - floor (- r)"
     1.6  
     1.7 -const_syntax (xsymbols)
     1.8 +notation (xsymbols)
     1.9    floor  ("\<lfloor>_\<rfloor>")
    1.10    ceiling  ("\<lceil>_\<rceil>")
    1.11  
    1.12 -const_syntax (HTML output)
    1.13 +notation (HTML output)
    1.14    floor  ("\<lfloor>_\<rfloor>")
    1.15    ceiling  ("\<lceil>_\<rceil>")
    1.16