| changeset 21199 | 2d83f93c3580 |
| parent 19984 | 29bb4659f80a |
| child 21215 | 7c9337a0e30a |
--- a/src/HOL/Finite_Set.thy Tue Nov 07 08:03:46 2006 +0100 +++ b/src/HOL/Finite_Set.thy Tue Nov 07 09:33:47 2006 +0100 @@ -1645,7 +1645,7 @@ done -lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::recpower)) = y^(card A)" +lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)" apply (erule finite_induct) apply (auto simp add: power_Suc) done