changeset 58447 | ea23ce403a3e |
parent 58395 | 7179d4da97fc |
child 58449 | e2d3c296b9fe |
--- a/src/Doc/Datatypes/Datatypes.thy Thu Sep 25 16:35:53 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Thu Sep 25 16:35:54 2014 +0200 @@ -1014,6 +1014,9 @@ (The @{text "[code]"} attribute is set by the @{text code} plugin, Section~\ref{ssec:code-generator}.) +\item[@{text "t."}\hthm{rec_transfer}\rm:] ~ \\ +@{thm list.rec_transfer[no_vars]} + \end{description} \end{indentblock}