diff -r 4d4521cbbcca -r ca761fe227d8 src/HOL/Real/RealOrd.thy
--- 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