# HG changeset patch
# User blanchet
# Date 1398241407 -7200
# Node ID efb39e0a89b0e8dfec041c9d4a7e1946f8489b4c
# Parent  41d3596d8a64f763a6c3f2555e65e863db46f33a
updated docs

diff -r 41d3596d8a64 -r efb39e0a89b0 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Apr 23 10:23:27 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Apr 23 10:23:27 2014 +0200
@@ -570,8 +570,8 @@
 *}
 
 
-subsubsection {* \keyw{datatype\_new\_compat}
-  \label{sssec:datatype-new-compat} *}
+subsubsection {* \keyw{datatype\_compat}
+  \label{sssec:datatype-compat} *}
 
 text {*
 \begin{matharray}{rcl}
@@ -593,10 +593,6 @@
 
 text {* \blankline *}
 
-    thm even_nat_odd_nat.size
-
-text {* \blankline *}
-
     ML {* Datatype_Data.get_info @{theory} @{type_name even_nat} *}
 
 text {*
@@ -971,8 +967,8 @@
 is recommended to use @{command datatype_compat} or \keyw{rep\_datatype}
 to register new-style datatypes as old-style datatypes.
 
-\item \emph{The constants @{text t_case} and @{text t_rec} are now called
-@{text case_t} and @{text rec_t}.}
+\item \emph{The constants @{text t_case}, @{text t_rec}, and @{text t_size} are
+now called @{text case_t}, @{text rec_t}, and @{text size_t}.}
 
 \item \emph{The recursor @{text rec_t} has a different signature for nested
 recursive datatypes.} In the old package, nested recursion through non-functions
@@ -994,12 +990,14 @@
 that unfold the definition of constants introduced by \keyw{datatype} will be
 difficult to port.
 
-\item \emph{Some induction rules have different names.}
+\item \emph{Some theorems have different names.}
 For non-mutually recursive datatypes,
 the alias @{text t.inducts} for @{text t.induct} is no longer generated.
 For $m > 1$ mutually recursive datatypes,
 @{text "t\<^sub>1_\<dots>_t\<^sub>m.inducts(i)"} has been renamed
-@{text "t\<^sub>i.induct"} for each @{text "i \<in> {1, \<dots>, t}"}.
+@{text "t\<^sub>i.induct"} for each @{text "i \<in> {1, \<dots>, t}"}, and similarly the
+collection @{text "t\<^sub>1_\<dots>_t\<^sub>m.size"} has been divided into @{text "t\<^sub>1.size"},
+\ldots, @{text "t\<^sub>m.size"}.
 
 \item \emph{The @{text t.simps} collection has been extended.}
 Previously available theorems are available at the same index.
@@ -1129,7 +1127,7 @@
 restrictions imposed on primitively recursive functions. The
 @{command datatype_compat} command is needed to register new-style datatypes
 for use with \keyw{fun} and \keyw{function}
-(Section~\ref{sssec:datatype-new-compat}):
+(Section~\ref{sssec:datatype-compat}):
 *}
 
     datatype_compat nat
@@ -2696,12 +2694,8 @@
 *}
 
 text {*
-%* primcorecursive and primcorec is unfinished
-%
 %* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting)
 %
-%* issues with HOL-Proofs?
-%
 %* partial documentation
 %
 %* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them
@@ -2714,6 +2708,8 @@
 %* in a locale, cannot use locally fixed types (because of limitation in typedef)?
 %
 % *names of variables suboptimal
+%
+% * in a locale, size is half broken
 *}
 *)