| changeset 58449 | e2d3c296b9fe |
| parent 58447 | ea23ce403a3e |
| child 58474 | 330ebcc3e77d |
--- 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}