equal
deleted
inserted
replaced
269 |
269 |
270 subsection {* Ceiling function *} |
270 subsection {* Ceiling function *} |
271 |
271 |
272 definition |
272 definition |
273 ceiling :: "'a::floor_ceiling \<Rightarrow> int" where |
273 ceiling :: "'a::floor_ceiling \<Rightarrow> int" where |
274 [code del]: "ceiling x = - floor (- x)" |
274 "ceiling x = - floor (- x)" |
275 |
275 |
276 notation (xsymbols) |
276 notation (xsymbols) |
277 ceiling ("\<lceil>_\<rceil>") |
277 ceiling ("\<lceil>_\<rceil>") |
278 |
278 |
279 notation (HTML output) |
279 notation (HTML output) |