# HG changeset patch
# User blanchet
# Date 1380546618 -7200
# Node ID 8ff43f638da233fedfb8d28bec61479910d7bb96
# Parent  c1097679e2955ad7460150e6c4aa8d573ce9b354
more "primrec_new" documentation

diff -r c1097679e295 -r 8ff43f638da2 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Sep 30 14:19:33 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Sep 30 15:10:18 2013 +0200
@@ -876,8 +876,8 @@
   \label{ssec:datatype-compatibility-issues} *}
 
 text {*
-The command @{command datatype_new} was designed to be highly compatible with
-\keyw{datatype}, to ease migration. There are nonetheless a number of
+The command @{command datatype_new} has been designed to be highly compatible
+with the old \keyw{datatype}, to ease migration. There are nonetheless a few
 incompatibilities that may arise when porting to the new package:
 
 \begin{itemize}
@@ -909,11 +909,11 @@
 difficult to port.
 
 \item \emph{A few theorems have different names.}
-The properties @{text t.cases} and @{text t.recs} have been renamed to
+The properties @{text t.cases} and @{text t.recs} have been renamed
 @{text t.case} and @{text t.rec}. For non-mutually recursive datatypes,
 @{text t.inducts} is available as @{text t.induct}.
 For $m > 1$ mutually recursive datatypes,
-@{text "t\<^sub>1_\<dots>_t\<^sub>m.inducts(i)"} has been renamed to
+@{text "t\<^sub>1_\<dots>_t\<^sub>m.inducts(i)"} has been renamed
 @{text "t\<^sub>i.induct"}.
 
 \item \emph{The @{text t.simps} collection has been extended.}
@@ -1316,20 +1316,23 @@
     by (cases xs) auto
 
 
-(*
 subsection {* Compatibility Issues
   \label{ssec:primrec-compatibility-issues} *}
 
 text {*
-%  * different induction in nested case
-%    * solution: define nested-as-mutual functions with primrec,
-%      and look at .induct
-%
-%  * different induction and recursor in nested case
-%    * only matters to low-level users; they can define a dummy function to force
-%      generation of mutualized recursor
+The command @{command primrec_new} has been designed to be highly compatible
+with the old \keyw{primrec}, to ease migration. There is nonetheless at least
+one incompatibility that may arise when porting to the new package:
+
+\begin{itemize}
+\setlength{\itemsep}{0pt}
+
+\item \emph{Theorems sometimes have different names.}
+For $m > 1$ mutually recursive functions,
+@{text "f\<^sub>1_\<dots>_f\<^sub>m.simps(k\<^sub>i,\<dots>,k\<^sub>i+n\<^sub>i-1)"} have
+been renamed @{text "f\<^sub>i.simps(1,\<dots>,n\<^sub>i-1)"}.
+\end{itemize}
 *}
-*)
 
 
 section {* Defining Codatatypes
@@ -1339,8 +1342,9 @@
 Codatatypes can be specified using the @{command codatatype} command. The
 command is first illustrated through concrete examples featuring different
 flavors of corecursion. More examples can be found in the directory
-\verb|~~/src/HOL/BNF/Examples|. The \emph{Archive of Formal Proofs} also
-includes some useful codatatypes, notably for lazy lists \cite{lochbihler-2010}.
+\verb|~~/src/HOL/|\allowbreak\verb|BNF/Examples|. The
+\emph{Archive of Formal Proofs} also includes some useful codatatypes, notably
+for lazy lists \cite{lochbihler-2010}.
 *}