| changeset 58094 | 117c5d2c2642 |
| parent 58044 | b5cdfb352814 |
| child 58096 | 5a48fef59fab |
--- 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]}