author | desharna |
Thu, 25 Sep 2014 16:35:56 +0200 | |
changeset 58449 | e2d3c296b9fe |
parent 58448 | a1d4e7473c98 |
child 58453 | 75b92e25f59f |
--- 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}