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