# HG changeset patch
# User desharna
# Date 1411655756 -7200
# Node ID e2d3c296b9fefa383f1463ecd88c38d55d409470
# Parent  a1d4e7473c980a8873bccf437fc3d123672033e8
document 'corec_transfer'

diff -r a1d4e7473c98 -r e2d3c296b9fe src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Sep 25 16:35:56 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Sep 25 16:35:56 2014 +0200
@@ -1845,6 +1845,9 @@
 @{thm llist.corec_sel(1)[no_vars]} \\
 @{thm llist.corec_sel(2)[no_vars]}
 
+\item[@{text "t."}\hthm{corec_transfer}\rm:] ~ \\
+@{thm llist.corec_transfer[no_vars]}
+
 \end{description}
 \end{indentblock}