Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Algebra/Divisibility.thy
changeset 50037 f2a32197a33a
parent 46129 229fcbebf732
child 53374 a14d2a854c02 
--- a/src/HOL/Algebra/Divisibility.thy	Thu Nov 08 19:55:37 2012 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Thu Nov 08 20:02:41 2012 +0100
@@ -244,7 +244,7 @@
  apply (elim dividesE, intro dividesI, assumption)
  apply (rule l_cancel[of c])
     apply (simp add: m_assoc carr)+
-apply (fast intro: divides_mult_lI carr)
+apply (fast intro: carr)
 done
 
 lemma (in comm_monoid) divides_mult_rI [intro]:
isabelle