# HG changeset patch
# User desharna
# Date 1404313311 -7200
# Node ID afc7081f19d40ec8a8a9b1b63b6786b811a6ef30
# Parent  8f0ba9f2d10ff92b98e77b9af3069d67710c5cde
document property 'corec_code'

diff -r 8f0ba9f2d10f -r afc7081f19d4 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Jul 02 17:01:49 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Jul 02 17:01:51 2014 +0200
@@ -1766,6 +1766,9 @@
 @{thm llist.corec(1)[no_vars]} \\
 @{thm llist.corec(2)[no_vars]}
 
+\item[@{text "t."}\hthm{corec\_code} @{text "[code]"}\rm:] ~ \\
+@{thm llist.corec_code[no_vars]}
+
 \item[@{text "t."}\hthm{disc\_corec}\rm:] ~ \\
 @{thm llist.disc_corec(1)[no_vars]} \\
 @{thm llist.disc_corec(2)[no_vars]}