--- a/src/Doc/Datatypes/Datatypes.thy Fri Nov 07 11:52:54 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Nov 07 11:52:56 2014 +0100
@@ -2873,11 +2873,15 @@
\item[@{text "t."}\hthm{size_gen_o_map}\rm:] ~ \\
@{thm list.size_gen_o_map[no_vars]}
+\item[@{text "t."}\hthm{size_neq}\rm:] ~ \\
+This property is missing for @{typ "'a list"}. If the @{term size} function
+always evaluate to a non-zero value, this theorem have the form
+@{prop "\<not> size x = 0"}.
+
\end{description}
\end{indentblock}
*}
-
subsection {* Transfer
\label{ssec:transfer} *}