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