isabelle: src/HOL/Hyperreal/HyperOrd.thy@30d9143aff7e (annotated)

10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	1	(* Title: Real/Hyperreal/HyperOrd.thy
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	2	Author: Jacques D. Fleuriot
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	3	Copyright: 2000 University of Edinburgh
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	4	Description: Type "hypreal" is a linear order and also
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	5	satisfies plus_ac0: + is an AC-operator with zero
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	6	*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	7
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	8	HyperOrd = HyperDef +
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	9
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	10	instance hypreal :: order (hypreal_le_refl,hypreal_le_trans,hypreal_le_anti_sym,hypreal_less_le)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	11	instance hypreal :: linorder (hypreal_le_linear)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	12
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	13	instance hypreal :: plus_ac0(hypreal_add_commute,hypreal_add_assoc,hypreal_add_zero_left)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	14
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	15	end

author	wenzelm
	Fri, 09 Nov 2001 22:52:38 +0100
changeset 12130	30d9143aff7e
parent 10751	a81ea5d3dd41
child 14297	7c84fd26add1
permissions	-rw-r--r--