| changeset 22274 | ce1459004c8d |
| parent 21404 | eb85850d3eb7 |
| child 23315 | df3a7e9ebadb |
--- a/src/HOL/NumberTheory/Int2.thy Wed Feb 07 17:46:03 2007 +0100 +++ b/src/HOL/NumberTheory/Int2.thy Wed Feb 07 17:51:38 2007 +0100 @@ -175,7 +175,7 @@ lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |] ==> zgcd (setprod id A,y) = 1" - by (induct set: Finites) (auto simp add: zgcd_zgcd_zmult) + by (induct set: finite) (auto simp add: zgcd_zgcd_zmult) subsection {* Some properties of MultInv *}