Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tweaked for times_ac1
authorpaulson
Fri, 05 Mar 2004 15:30:49 +0100
changeset 14439 0f626a712456
parent 14438 6b41e98931f8
child 14440 3d6ed7eedfc8
tweaked for times_ac1
src/HOL/Algebra/abstract/Ring.thy file | annotate | diff | comparison | revisions 
--- 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]:
isabelle