# HG changeset patch
# User blanchet
# Date 1420448080 -3600
# Node ID 3a3e6e9c289f8afed6b9f9bdddf299c68f2926a2
# Parent  53c315d87606a8eae29ddd2c80d7de6fd7e515a3
docs

diff -r 53c315d87606 -r 3a3e6e9c289f src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Jan 05 06:56:15 2015 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Jan 05 09:54:40 2015 +0100
@@ -1519,8 +1519,9 @@
 warning that is normally emitted when some constructors are missing.
 
 \item
-The @{text "transfer"} option indicates that a transfer rule should be
-generated and registered as such for use by the Transfer tool.
+The @{text "transfer"} option indicates that an unconditional transfer rule
+should be generated and proved @{text "by transfer_prover"}. The
+@{text "[transfer_rule]"} attribute is set on the generated theorem.
 \end{itemize}
 
 %%% TODO: elaborate on format of the equations
@@ -2468,8 +2469,9 @@
 expressed using the constructor or destructor view cover all possible cases.
 
 \item
-The @{text "transfer"} option indicates that a transfer rule should be
-generated and registered as such for use by the Transfer tool.
+The @{text "transfer"} option indicates that an unconditional transfer rule
+should be generated and proved @{text "by transfer_prover"}. The
+@{text "[transfer_rule]"} attribute is set on the generated theorem.
 \end{itemize}
 
 The @{command primcorec} command is an abbreviation for @{command