# HG changeset patch
# User wenzelm
# Date 1231545992 -3600
# Node ID 948d616959e4dc19fe34a0fe1f59f77583ad4d1e
# Parent  43a12fc76f4897e9e9b46a6a6d04ecbd396da21c
fixed proof involving dvd;

diff -r 43a12fc76f48 -r 948d616959e4 src/HOL/Algebra/IntRing.thy
--- 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: