merged

--- a/src/HOL/Algebra/IntRing.thy	Sat Jan 10 01:28:18 2009 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Sat Jan 10 01:28:31 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: