Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed proof involving dvd;
authorwenzelm
Sat, 10 Jan 2009 01:06:32 +0100
changeset 29424 948d616959e4
parent 29413 43a12fc76f48
child 29425 6baa02c8263e
fixed proof involving dvd;
src/HOL/Algebra/IntRing.thy file | annotate | diff | comparison | revisions 
--- 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:
isabelle