# HG changeset patch
# User blanchet
# Date 1412244149 -7200
# Node ID 251fc4a5170070d53f876817d68484046307f27f
# Parent  cb68c3f564fe53c0173562bd39452d2ce1dac0a8
documentation

diff -r cb68c3f564fe -r 251fc4a51700 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Oct 02 12:02:28 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Oct 02 12:02:29 2014 +0200
@@ -2824,6 +2824,11 @@
 
 \end{description}
 \end{indentblock}
+
+In addition, the plugin sets the @{text "[code]"} attribute on a number of
+properties of (co)datatypes and other freely generated types, as documented in
+Sections \ref{ssec:datatype-generated-theorems} and
+\ref{ssec:codatatype-generated-theorems}.
 *}
 
 
@@ -2853,7 +2858,6 @@
 
 \item[@{text "t."}\hthm{size_o_map}\rm:] ~ \\
 @{thm list.size_o_map[no_vars]}
-(This property is not generated for all datatypes.)
 
 \end{description}
 \end{indentblock}