# HG changeset patch
# User blanchet
# Date 1411051660 -7200
# Node ID 1b4d31b7bd105aabdf11fc2d5b22cef6f303561b
# Parent  4bdd00a76e54c4073dbebda78042b042d5357a6d
fixed attribute name in docs (thanks to Andreas Lochbihler)

diff -r 4bdd00a76e54 -r 1b4d31b7bd10 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Sep 18 16:47:40 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Sep 18 16:47:40 2014 +0200
@@ -2877,22 +2877,22 @@
 \item[@{text "t."}\hthm{rel_eq_onp}\rm:] ~ \\
 @{thm list.rel_eq_onp[no_vars]}
 
-\item[@{text "t."}\hthm{left_total_rel} @{text "[transfer]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{left_total_rel} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.left_total_rel[no_vars]}
 
-\item[@{text "t."}\hthm{left_unique_rel} @{text "[transfer]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{left_unique_rel} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.left_unique_rel[no_vars]}
 
-\item[@{text "t."}\hthm{right_total_rel} @{text "[transfer]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{right_total_rel} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.right_total_rel[no_vars]}
 
-\item[@{text "t."}\hthm{right_unique_rel} @{text "[transfer]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{right_unique_rel} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.right_unique_rel[no_vars]}
 
-\item[@{text "t."}\hthm{bi_total_rel} @{text "[transfer]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{bi_total_rel} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.bi_total_rel[no_vars]}
 
-\item[@{text "t."}\hthm{bi_unique_rel} @{text "[transfer]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{bi_unique_rel} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.bi_unique_rel[no_vars]}
 
 \end{description}