# 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]}