--- a/src/HOL/Big_Operators.thy Tue Mar 23 22:43:53 2010 +0100
+++ b/src/HOL/Big_Operators.thy Tue Mar 23 19:03:05 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
--- a/src/HOLCF/Fix.thy Tue Mar 23 22:43:53 2010 +0100
+++ b/src/HOLCF/Fix.thy Tue Mar 23 19:03:05 2010 -0700
@@ -6,7 +6,7 @@
header {* Fixed point operator and admissibility *}
theory Fix
-imports Cfun Cprod
+imports Cfun
begin
defaultsort pcpo
--- a/src/HOLCF/Fixrec.thy Tue Mar 23 22:43:53 2010 +0100
+++ b/src/HOLCF/Fixrec.thy Tue Mar 23 19:03:05 2010 -0700
@@ -5,7 +5,7 @@
header "Package for defining recursive functions in HOLCF"
theory Fixrec
-imports Sprod Ssum Up One Tr Fix
+imports Cprod Sprod Ssum Up One Tr Fix
uses
("Tools/holcf_library.ML")
("Tools/fixrec.ML")