changeset 14738 | 83f1a514dcb4 |
parent 14723 | b77ce15b625a |
child 15481 | fc075ae929e4 |
--- a/src/HOL/Algebra/poly/LongDiv.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Algebra/poly/LongDiv.thy Tue May 11 20:11:08 2004 +0200 @@ -22,7 +22,7 @@ apply (simp) apply (force) apply (simp) - apply (subst plus_ac0.commute[of m]) + apply (subst ab_semigroup_add.add_commute[of m]) apply (simp) done