# HG changeset patch
# User desharna
# Date 1408459593 -7200
# Node ID 52181f7b4468922ee72dbae7b3dfbd0288ae9598
# Parent  412ec967e3b3d4bb217a8449e9b9ee6febb6618d
document 'ctr_transfer'

diff -r 412ec967e3b3 -r 52181f7b4468 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Aug 19 16:46:31 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Aug 19 16:46:33 2014 +0200
@@ -856,6 +856,10 @@
 \begin{indentblock}
 \begin{description}
 
+\item[@{text "t."}\hthm{ctr_transfer}\rm:] ~ \\
+@{thm list.ctr_transfer(1)[no_vars]} \\
+@{thm list.ctr_transfer(2)[no_vars]}
+
 \item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\
 @{thm list.set(1)[no_vars]} \\
 @{thm list.set(2)[no_vars]}