equal
deleted
inserted
replaced
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 |
|