# HG changeset patch
# User huffman
# Date 1269372027 25200
# Node ID 93faaa15c3d5de5be8c79bc332307d3dc49881d5
# Parent  5f38ae62d93940a867044cdd2abf4965c9804a69
sublocale comm_monoid_add < setprod --> sublocale comm_monoid_mult < setprod

diff -r 5f38ae62d939 -r 93faaa15c3d5 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Tue Mar 23 19:35:33 2010 +0100
+++ b/src/HOL/Big_Operators.thy	Tue Mar 23 12:20:27 2010 -0700
@@ -804,7 +804,7 @@
 definition (in comm_monoid_mult) setprod :: "('b \<Rightarrow> 'a) => 'b set => 'a" where
   "setprod f A = (if finite A then fold_image (op *) f 1 A else 1)"
 
-sublocale comm_monoid_add < setprod!: comm_monoid_big "op *" 1 setprod proof
+sublocale comm_monoid_mult < setprod!: comm_monoid_big "op *" 1 setprod proof
 qed (fact setprod_def)
 
 abbreviation