# HG changeset patch
# User desharna
# Date 1408015279 -7200
# Node ID f620851148a96a489c1c3cbf09c8190ff39af0e7
# Parent  c29659f77f8d3766d016e8a7d009ee07acac085e
document property 'rel_map'

diff -r c29659f77f8d -r f620851148a9 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Aug 14 13:20:54 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Aug 14 13:21:19 2014 +0200
@@ -943,6 +943,10 @@
 \item[@{text "t."}\hthm{rel_flip}\rm:] ~ \\
 @{thm list.rel_flip[no_vars]}
 
+\item[@{text "t."}\hthm{rel_map}\rm:] ~ \\
+@{thm list.rel_map(1)[no_vars]} \\
+@{thm list.rel_map(2)[no_vars]}
+
 \item[@{text "t."}\hthm{rel_mono}\rm:] ~ \\
 @{thm list.rel_mono[no_vars]}