src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Wed May 24 18:46:38 2000 +0200
+++ b/src/HOL/HOL.thy	Wed May 24 18:47:43 2000 +0200
@@ -68,6 +68,10 @@
   *             :: "['a::times, 'a] => 'a"          (infixl 70)
   (*See Nat.thy for "^"*)
 
+axclass plus_ac0 < plus, zero
+    commute: "x + y = y + x"
+    assoc:   "(x + y) + z = x + (y + z)"
+    zero:    "0 + x = x"
 
 
 (** Additional concrete syntax **)