# HG changeset patch
# User krauss
# Date 1248763728 -7200
# Node ID 64660a887b1597932010e876a5b390bfbbc583d5
# Parent  8467626b394e8a2a266e136e4a978dd9e30b5dc7
adapted doc to type of "op O"

diff -r 8467626b394e -r 64660a887b15 doc-src/Main/Docs/Main_Doc.thy
--- a/doc-src/Main/Docs/Main_Doc.thy	Tue Jul 28 00:31:48 2009 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy	Tue Jul 28 08:48:48 2009 +0200
@@ -220,7 +220,7 @@
 
 \begin{supertabular}{@ {} l @ {~::~} l @ {}}
 @{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\
-@{const Relation.rel_comp} & @{term_type_only Relation.rel_comp "('a*'b)set\<Rightarrow>('c*'a)set\<Rightarrow>('c*'b)set"}\\
+@{const Relation.rel_comp} & @{term_type_only Relation.rel_comp "('a*'b)set\<Rightarrow>('b*'c)set\<Rightarrow>('a*'c)set"}\\
 @{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\<Rightarrow>'a set\<Rightarrow>'b set"}\\
 @{const Relation.inv_image} & @{term_type_only Relation.inv_image "('a*'a)set\<Rightarrow>('b\<Rightarrow>'a)\<Rightarrow>('b*'b)set"}\\
 @{const Relation.Id_on} & @{term_type_only Relation.Id_on "'a set\<Rightarrow>('a*'a)set"}\\