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/GCD.thy
changeset 63882 018998c00003
parent 63489 cd540c8031a4
child 63915 bab633745c7f 
--- a/src/HOL/GCD.thy	Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/GCD.thy	Thu Sep 15 11:48:20 2016 +0200
@@ -865,7 +865,7 @@
     apply (auto simp add: gcd_mult_cancel)
   done
 
-lemma listprod_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (listprod xs) y"
+lemma prod_list_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (prod_list xs) y"
   by (induct xs) (simp_all add: gcd_mult_cancel)
 
 lemma coprime_divisors:
isabelle