--- a/doc-src/Main/Docs/Main_Doc.thy Wed Aug 11 11:52:40 2010 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy Wed Aug 11 11:56:57 2010 +0200
@@ -109,7 +109,7 @@
@{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\
@{const Set.insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\
@{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\
-@{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\texttt{:})\\
+@{const Set.member} & @{term_type_only Set.member "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\texttt{:})\\
@{const Set.union} & @{term_type_only Set.union "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Un})\\
@{const Set.inter} & @{term_type_only Set.inter "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Int})\\
@{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\