# HG changeset patch
# User desharna
# Date 1415357576 -3600
# Node ID 0ef44616fd5fbb79c18cfa53b0ecd0d231523dd2
# Parent  5be251101978ca55877854e8ca605ffee4c6c9ff
document 'size_neq'

diff -r 5be251101978 -r 0ef44616fd5f src/Doc/Datatypes/Datatypes.thy
--- 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} *}