equal
deleted
inserted
replaced
141 |
141 |
142 subsection {* Floor function *} |
142 subsection {* Floor function *} |
143 |
143 |
144 definition |
144 definition |
145 floor :: "'a::archimedean_field \<Rightarrow> int" where |
145 floor :: "'a::archimedean_field \<Rightarrow> int" where |
146 "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))" |
146 [code del]: "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))" |
147 |
147 |
148 notation (xsymbols) |
148 notation (xsymbols) |
149 floor ("\<lfloor>_\<rfloor>") |
149 floor ("\<lfloor>_\<rfloor>") |
150 |
150 |
151 notation (HTML output) |
151 notation (HTML output) |
272 |
272 |
273 subsection {* Ceiling function *} |
273 subsection {* Ceiling function *} |
274 |
274 |
275 definition |
275 definition |
276 ceiling :: "'a::archimedean_field \<Rightarrow> int" where |
276 ceiling :: "'a::archimedean_field \<Rightarrow> int" where |
277 "ceiling x = - floor (- x)" |
277 [code del]: "ceiling x = - floor (- x)" |
278 |
278 |
279 notation (xsymbols) |
279 notation (xsymbols) |
280 ceiling ("\<lceil>_\<rceil>") |
280 ceiling ("\<lceil>_\<rceil>") |
281 |
281 |
282 notation (HTML output) |
282 notation (HTML output) |