# HG changeset patch
# User blanchet
# Date 1410772209 -7200
# Node ID a7add8066122ccf77815448f2e7ee9b9d84b596c
# Parent  a5a3b576fcfb8978fcd9de65eae64b9ffabbca26
document size difference

diff -r a5a3b576fcfb -r a7add8066122 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Sep 15 10:49:07 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Sep 15 11:10:09 2014 +0200
@@ -1065,6 +1065,11 @@
 functions, the old-style induction rule can be obtained by applying the
 @{text "[unfolded all_mem_range]"} attribute on @{text t.induct}.
 
+\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"}.
+
 \item \emph{The internal constructions are completely different.} Proof texts
 that unfold the definition of constants introduced by \keyw{old_datatype} will
 be difficult to port.