author | kleing |
Sat, 01 Mar 2003 16:45:51 +0100 | |
changeset 13840 | 399c8103a98f |
parent 10751 | a81ea5d3dd41 |
child 14297 | 7c84fd26add1 |
permissions | -rw-r--r-- |
(* 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