document 'map_o_corec'
authordesharna
Tue, 21 Oct 2014 17:23:13 +0200
changeset 58735 919186869943
parent 58734 20235f0512e2
child 58736 552ccec3f00f
document 'map_o_corec'
src/Doc/Datatypes/Datatypes.thy
--- 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]}