| changeset 57514 | bdc2c6b40bf2 |
| parent 57512 | cc97b347b301 |
| child 60112 | 3eab4acaa035 |
--- a/src/HOL/Algebra/IntRing.thy Sat Jul 05 10:09:01 2014 +0200 +++ b/src/HOL/Algebra/IntRing.thy Sat Jul 05 11:01:53 2014 +0200 @@ -290,7 +290,7 @@ apply (subst int_Idl_subset_ideal, subst int_Idl, simp) apply (rule, clarify) apply (simp add: dvd_def) - apply (simp add: dvd_def mult_ac) + apply (simp add: dvd_def ac_simps) done lemma dvds_eq_Idl: "l dvd k \<and> k dvd l \<longleftrightarrow> Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}"