src/HOL/Real/Hyperreal/HyperOrd.thy
changeset 10045 c76b73e16711
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/Hyperreal/HyperOrd.thy	Thu Sep 21 12:17:11 2000 +0200
     1.3 @@ -0,0 +1,15 @@
     1.4 +(*  Title:	 Real/Hyperreal/HyperOrd.thy
     1.5 +    Author:      Jacques D. Fleuriot
     1.6 +    Copyright:   2000 University of Edinburgh
     1.7 +    Description: Type "hypreal" is a linear order and also 
     1.8 +                 satisfies plus_ac0: + is an AC-operator with zero
     1.9 +*)
    1.10 +
    1.11 +HyperOrd = HyperDef +
    1.12 +
    1.13 +instance hypreal :: order (hypreal_le_refl,hypreal_le_trans,hypreal_le_anti_sym,hypreal_less_le)
    1.14 +instance hypreal :: linorder (hypreal_le_linear)
    1.15 +
    1.16 +instance hypreal :: plus_ac0(hypreal_add_commute,hypreal_add_assoc,hypreal_add_zero_left)
    1.17 +
    1.18 +end