isabelle: src/HOL/Hyperreal/IntFloor.thy@ad66687ece6e (annotated)

13958 c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: diff changeset	1	(* Title: IntFloor.thy
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: diff changeset	2	Author: Jacques D. Fleuriot
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: diff changeset	3	Copyright: 2001,2002 University of Edinburgh
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: diff changeset	4	Description: Floor and ceiling operations over reals
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: diff changeset	5	*)
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: diff changeset	6
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: diff changeset	7	IntFloor = Integration +
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: diff changeset	8
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: diff changeset	9	constdefs
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: diff changeset	10
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: diff changeset	11	floor :: real => int
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: diff changeset	12	"floor r == (LEAST n. r < real (n + (1::int)))"
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: diff changeset	13
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: diff changeset	14	ceiling :: real => int
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: diff changeset	15	"ceiling r == - floor (- r)"
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: diff changeset	16
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: diff changeset	17	end

author	paulson
	Fri, 05 Dec 2003 18:10:59 +0100
changeset 14277	ad66687ece6e
parent 13958	c1c67582c9b5
child 14425	0a76d4633bb6
permissions	-rw-r--r--