# HG changeset patch
# User haftmann
# Date 1281520617 -7200
# Node ID dc2a61b98bab5de24134789eae18cd77e8fd9742
# Parent  5888841c38da0f3c32fe515f123e00fbd5c5070e
avoid old unnamed infix

diff -r 5888841c38da -r dc2a61b98bab doc-src/Main/Docs/Main_Doc.thy
--- 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"}\\