# HG changeset patch
# User haftmann
# Date 1268718901 -3600
# Node ID 1c4a8d3b26d2b505ae046a7165864d40eb60b99e
# Parent  4046a6111838de06a186620727a74d83f17be132
adjusted to changes in Finite_Set

diff -r 4046a6111838 -r 1c4a8d3b26d2 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}