| author | kleing |
| Tue, 13 May 2003 08:59:21 +0200 | |
| changeset 14024 | 213dcc39358f |
| parent 13958 | c1c67582c9b5 |
| child 14425 | 0a76d4633bb6 |
| permissions | -rw-r--r-- |
| 13958 | 1 |
(* Title: IntFloor.thy |
2 |
Author: Jacques D. Fleuriot |
|
3 |
Copyright: 2001,2002 University of Edinburgh |
|
4 |
Description: Floor and ceiling operations over reals |
|
5 |
*) |
|
6 |
||
7 |
IntFloor = Integration + |
|
8 |
||
9 |
constdefs |
|
10 |
||
11 |
floor :: real => int |
|
12 |
"floor r == (LEAST n. r < real (n + (1::int)))" |
|
13 |
||
14 |
ceiling :: real => int |
|
15 |
"ceiling r == - floor (- r)" |
|
16 |
||
17 |
end |