# HG changeset patch
# User wenzelm
# Date 1231547311 -3600
# Node ID 6baa02c8263e687a37fc1e24c90b8d6680d2b083
# Parent  948d616959e4dc19fe34a0fe1f59f77583ad4d1e# Parent  75ac4d6ff8fb64e9aa74779845ee64b767070060
merged

diff -r 75ac4d6ff8fb -r 6baa02c8263e src/HOL/Algebra/IntRing.thy
--- 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: