# HG changeset patch
# User wenzelm
# Date 1335124905 -7200
# Node ID 8e2e87a0a59484200feb93c1c458f9d08d11fa83
# Parent  d9a1b706d5698f601a702d75e159673e06481f25
updated const "relcomp";

diff -r d9a1b706d569 -r 8e2e87a0a594 doc-src/Main/Docs/Main_Doc.thy
--- a/doc-src/Main/Docs/Main_Doc.thy	Sun Apr 22 21:47:32 2012 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy	Sun Apr 22 22:01:45 2012 +0200
@@ -243,7 +243,7 @@
 
 \begin{tabular}{@ {} 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>('b*'c)set\<Rightarrow>('a*'c)set"}\\
+@{const Relation.relcomp} & @{term_type_only Relation.relcomp "('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"}\\