changeset 43733 | a6ca7b83612f |
parent 43732 | 6b2bdc57155b |
child 47108 | 2a1953f0d20d |
--- a/src/HOL/Archimedean_Field.thy Sat Jul 09 13:41:58 2011 +0200 +++ b/src/HOL/Archimedean_Field.thy Sat Jul 09 19:28:33 2011 +0200 @@ -271,7 +271,7 @@ definition ceiling :: "'a::floor_ceiling \<Rightarrow> int" where - [code del]: "ceiling x = - floor (- x)" + "ceiling x = - floor (- x)" notation (xsymbols) ceiling ("\<lceil>_\<rceil>")