| changeset 58735 | 919186869943 |
| parent 58733 | 797d0e7aefc7 |
| child 58737 | b45405874f8f |
--- a/src/Doc/Datatypes/Datatypes.thy Tue Oct 21 17:23:12 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Tue Oct 21 17:23:13 2014 +0200 @@ -1855,6 +1855,9 @@ @{thm llist.corec_sel(1)[no_vars]} \\ @{thm llist.corec_sel(2)[no_vars]} +\item[@{text "t."}\hthm{map_o_corec}\rm:] ~ \\ +@{thm llist.map_o_corec[no_vars]} + \item[@{text "t."}\hthm{corec_transfer}\rm:] ~ \\ @{thm llist.corec_transfer[no_vars]}