# HG changeset patch
# User haftmann
# Date 1248357554 -7200
# Node ID 0ddf61f96b2af9204e6ea63de150696f83b6b003
# Parent  31cd1ea502aa333151aa83af7cdc82dd6ca9d060
fixed doc

diff -r 31cd1ea502aa -r 0ddf61f96b2a doc-src/Main/Docs/Main_Doc.thy
--- a/doc-src/Main/Docs/Main_Doc.thy	Thu Jul 23 09:38:22 2009 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy	Thu Jul 23 15:59:14 2009 +0200
@@ -107,11 +107,11 @@
 
 \begin{supertabular}{@ {} l @ {~::~} l l @ {}}
 @{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\
-@{const insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'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.Un} & @{term_type_only Set.Un "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Un})\\
-@{const Set.Int} & @{term_type_only Set.Int "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Int})\\
+@{const Set.union} & @{term_type_only Set.Un "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Un})\\
+@{const Set.inter} & @{term_type_only Set.Int "'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"}\\
 @{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
 @{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\