# HG changeset patch
# User paulson
# Date 1078497049 -3600
# Node ID 0f626a71245636e416f97cb7273f37f7c9f04209
# Parent  6b41e98931f8e97ba3bc755be37f67e0ccecc5f1
tweaked for times_ac1

diff -r 6b41e98931f8 -r 0f626a712456 src/HOL/Algebra/abstract/Ring.thy
--- a/src/HOL/Algebra/abstract/Ring.thy	Fri Mar 05 15:26:14 2004 +0100
+++ b/src/HOL/Algebra/abstract/Ring.thy	Fri Mar 05 15:30:49 2004 +0100
@@ -129,7 +129,7 @@
 proof (induct n)
   case 0 show ?case by simp
 next
-  case Suc thus ?case by (simp add: assoc) 
+  case Suc thus ?case by (simp add: plus_ac0.assoc) 
 qed
 
 lemma natsum_cong [cong]: