| changeset 15392 | 290bc97038c7 |
| parent 14981 | e73f8140af78 |
| child 16417 | 9bc16273c2d4 |
--- a/src/HOL/NumberTheory/Int2.thy Thu Dec 09 16:45:46 2004 +0100 +++ b/src/HOL/NumberTheory/Int2.thy Thu Dec 09 18:30:59 2004 +0100 @@ -178,7 +178,7 @@ by (frule_tac m = m in zcong_not_zero, auto) lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |] - ==> zgcd (gsetprod id A,y) = 1"; + ==> zgcd (setprod id A,y) = 1"; by (induct set: Finites, auto simp add: zgcd_zgcd_zmult) (*****************************************************************)