changeset 29424 | 948d616959e4 |
parent 29242 | e190bc2a5399 |
child 29700 | 22faf21db3df |
--- a/src/HOL/Algebra/IntRing.thy Fri Jan 09 09:49:01 2009 -0800 +++ b/src/HOL/Algebra/IntRing.thy Sat Jan 10 01:06:32 2009 +0100 @@ -348,8 +348,8 @@ "(Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) = (l dvd k)" apply (subst int_Idl_subset_ideal, subst int_Idl, simp) apply (rule, clarify) -apply (simp add: dvd_def, clarify) -apply (simp add: int.m_comm) +apply (simp add: dvd_def) +apply (simp add: dvd_def mult_ac) done lemma dvds_eq_Idl: