# HG changeset patch
# User desharna
# Date 1413904993 -7200
# Node ID 91918686994338196b4216c832135471520e861e
# Parent  20235f0512e2af5d9a08f238981121519c04e574
document 'map_o_corec'

diff -r 20235f0512e2 -r 919186869943 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]}