adjusted to changes in Finite_Set
authorhaftmann
Tue, 16 Mar 2010 06:55:01 +0100
changeset 35805 1c4a8d3b26d2
parent 35804 4046a6111838
child 35806 a814cccce0b8
adjusted to changes in Finite_Set
doc-src/Main/Docs/Main_Doc.thy
--- a/doc-src/Main/Docs/Main_Doc.thy	Mon Mar 15 22:22:28 2010 +0100
+++ b/doc-src/Main/Docs/Main_Doc.thy	Tue Mar 16 06:55:01 2010 +0100
@@ -396,8 +396,8 @@
 @{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set => nat"}\\
 @{const Finite_Set.fold} & @{term_type_only Finite_Set.fold "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\
 @{const Finite_Set.fold_image} & @{typ "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\
-@{const Finite_Set.setsum} & @{term_type_only Finite_Set.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\
-@{const Finite_Set.setprod} & @{term_type_only Finite_Set.setprod "('a => 'b) => 'a set => 'b::comm_monoid_mult"}\\
+@{const Big_Operators.setsum} & @{term_type_only Big_Operators.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\
+@{const Big_Operators.setprod} & @{term_type_only Big_Operators.setprod "('a => 'b) => 'a set => 'b::comm_monoid_mult"}\\
 \end{supertabular}