author | paulson |
Fri, 21 Nov 2003 11:15:40 +0100 | |
changeset 14265 | 95b42e69436c |
parent 13958 | c1c67582c9b5 |
child 14425 | 0a76d4633bb6 |
permissions | -rw-r--r-- |
(* Title: IntFloor.thy Author: Jacques D. Fleuriot Copyright: 2001,2002 University of Edinburgh Description: Floor and ceiling operations over reals *) IntFloor = Integration + constdefs floor :: real => int "floor r == (LEAST n. r < real (n + (1::int)))" ceiling :: real => int "ceiling r == - floor (- r)" end