document property 'rel_map'

--- 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]}