--- a/src/Doc/Datatypes/Datatypes.thy Sat Apr 18 23:43:30 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Sun Apr 19 15:38:24 2015 +0100
@@ -3034,7 +3034,7 @@
text {*
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
+@{text "size \<Colon> t \<Rightarrow> nat"} belonging to the @{text size} type
class. The \keyw{fun} command relies on @{const size} to prove termination of
recursive functions on datatypes.
@@ -3058,7 +3058,7 @@
\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
+always evaluates to a non-zero value, this theorem has the form
@{prop "\<not> size x = 0"}.
\end{description}