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