# HG changeset patch
# User desharna
# Date 1409314885 -7200
# Node ID 117c5d2c26428aa9b9b57421034247828a1d39a5
# Parent  6f37a300c82b226297891c57ae0e6486e4722fe3
document 'case_transfer'

diff -r 6f37a300c82b -r 117c5d2c2642 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Aug 29 14:21:24 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Aug 29 14:21:25 2014 +0200
@@ -856,6 +856,9 @@
 \begin{indentblock}
 \begin{description}
 
+\item[@{text "t."}\hthm{case_transfer}\rm:] ~ \\
+@{thm list.case_transfer[no_vars]}
+
 \item[@{text "t."}\hthm{ctr_transfer}\rm:] ~ \\
 @{thm list.ctr_transfer(1)[no_vars]} \\
 @{thm list.ctr_transfer(2)[no_vars]}