Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Hyperreal/HyperOrd.thy
author wenzelm
Tue, 19 Feb 2002 23:45:54 +0100
changeset 12899 7d5b690253ee
parent 10751 a81ea5d3dd41
child 14297 7c84fd26add1
permissions -rw-r--r--
"isatool usedir -D output HOL Test && isatool document Test/output";

(*  Title:	 Real/Hyperreal/HyperOrd.thy
    Author:      Jacques D. Fleuriot
    Copyright:   2000 University of Edinburgh
    Description: Type "hypreal" is a linear order and also 
                 satisfies plus_ac0: + is an AC-operator with zero
*)

HyperOrd = HyperDef +

instance hypreal :: order (hypreal_le_refl,hypreal_le_trans,hypreal_le_anti_sym,hypreal_less_le)
instance hypreal :: linorder (hypreal_le_linear)

instance hypreal :: plus_ac0(hypreal_add_commute,hypreal_add_assoc,hypreal_add_zero_left)

end
isabelle