# HG changeset patch
# User wenzelm
# Date 1003170852 -7200
# Node ID 37efbe093d3c20348031a794aa21619dda4e0d78
# Parent  b03c8a3fcc6dd250e4efb982387f008860de4c56
ring includes plus_ac0;

diff -r b03c8a3fcc6d -r 37efbe093d3c src/HOL/Algebra/abstract/Ring.ML
--- 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 =
diff -r b03c8a3fcc6d -r 37efbe093d3c src/HOL/Algebra/abstract/Ring.thy
--- 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"