--- a/src/HOL/Real/RealOrd.thy Wed Jun 07 12:07:07 2000 +0200
+++ b/src/HOL/Real/RealOrd.thy Wed Jun 07 12:14:18 2000 +0200
@@ -2,7 +2,8 @@
ID: $Id$
Author: Jacques D. Fleuriot and Lawrence C. Paulson
Copyright: 1998 University of Cambridge
- Description: Type "real" is a linear order
+ Description: Type "real" is a linear order and also
+ satisfies plus_ac0: + is an AC-operator with zero
*)
RealOrd = RealDef +
@@ -10,4 +11,6 @@
instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le)
instance real :: linorder (real_le_linear)
+instance real :: plus_ac0 (real_add_commute,real_add_assoc,real_add_zero_left)
+
end