ring includes plus_ac0;

--- a/src/HOL/Algebra/abstract/Ring.ML	Mon Oct 15 20:33:42 2001 +0200
+++ b/src/HOL/Algebra/abstract/Ring.ML	Mon Oct 15 20:34:12 2001 +0200
@@ -6,6 +6,10 @@
 
 Blast.overloaded ("Divides.op dvd", domain_type);
 
+val a_assoc = thm "plus_ac0.assoc";
+val l_zero = thm "plus_ac0.zero";
+val a_comm = thm "plus_ac0.commute";
+
 section "Rings";
 
 fun make_left_commute assoc commute s =

--- a/src/HOL/Algebra/abstract/Ring.thy	Mon Oct 15 20:33:42 2001 +0200
+++ b/src/HOL/Algebra/abstract/Ring.thy	Mon Oct 15 20:34:12 2001 +0200
@@ -27,12 +27,12 @@
 (* Class ring and ring axioms *)
 
 axclass
-  ring < ringS
+  ring < ringS, plus_ac0
 
-  a_assoc	"(a + b) + c = a + (b + c)"
-  l_zero	"0 + a = a"
+(*a_assoc	"(a + b) + c = a + (b + c)"*)
+(*l_zero	"0 + a = a"*)
   l_neg		"(-a) + a = 0"
-  a_comm	"a + b = b + a"
+(*a_comm	"a + b = b + a"*)
 
   m_assoc	"(a * b) * c = a * (b * c)"
   l_one		"<1> * a = a"