equal
deleted
inserted
replaced
74 syntax |
74 syntax |
75 "_msetprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" |
75 "_msetprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" |
76 ("(3PROD _:#_. _)" [0, 51, 10] 10) |
76 ("(3PROD _:#_. _)" [0, 51, 10] 10) |
77 |
77 |
78 translations |
78 translations |
79 "PROD i :# A. b" == "msetprod (%i. b) A" |
79 "PROD i :# A. b" == "CONST msetprod (%i. b) A" |
80 |
80 |
81 lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" |
81 lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" |
82 apply (simp add: msetprod_def power_add) |
82 apply (simp add: msetprod_def power_add) |
83 apply (subst setprod_Un2) |
83 apply (subst setprod_Un2) |
84 apply auto |
84 apply auto |