# HG changeset patch
# User desharna
# Date 1413904994 -7200
# Node ID b45405874f8fa3b49e423e7087ecca368032a431
# Parent  552ccec3f00fb9e277abffb7db652325c9430bc3
document 'size_gen'

diff -r 552ccec3f00f -r b45405874f8f src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Oct 21 17:23:13 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Oct 21 17:23:14 2014 +0200
@@ -1081,7 +1081,7 @@
 \item \emph{The @{const size} function has a slightly different definition.}
 The new function returns @{text 1} instead of @{text 0} for some nonrecursive
 constructors. This departure from the old behavior made it possible to implement
-@{const size} in terms of the parameterized function @{text "t.size_t"}.
+@{const size} in terms of the generic function @{text "t.size_t"}.
 Moreover, the new function considers nested occurrences of a value, in the nested
 recursive case. The old behavior can be obtained by disabling the @{text size}
 plugin (Section~\ref{sec:controlling-plugins}) and instantiating the
@@ -2849,7 +2849,7 @@
   \label{ssec:size} *}
 
 text {*
-For each datatype, the \hthm{size} plugin generates a parameterized size
+For each datatype, the \hthm{size} plugin generates a generic size
 function @{text "t.size_t"} as well as a specific instance
 @{text "size \<Colon> t \<Rightarrow> bool"} belonging to the @{text size} type
 class. The \keyw{fun} command relies on @{const size} to prove termination of
@@ -2866,6 +2866,10 @@
 @{thm list.size(3)[no_vars]} \\
 @{thm list.size(4)[no_vars]}
 
+\item[@{text "t."}\hthm{size_gen}\rm:] ~ \\
+@{thm list.size_gen(1)[no_vars]} \\
+@{thm list.size_gen(2)[no_vars]}
+
 \item[@{text "t."}\hthm{size_o_map}\rm:] ~ \\
 @{thm list.size_o_map[no_vars]}