# HG changeset patch
# User blanchet
# Date 1410454476 -7200
# Node ID 068496644aa15da9af25f69db205b96448ef66b9
# Parent  e3a01b73579fc2f74f9191e5e61862dd7455574b
more docs

diff -r e3a01b73579f -r 068496644aa1 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Sep 11 15:08:56 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Sep 11 18:54:36 2014 +0200
@@ -88,7 +88,7 @@
 \cite{mgordon79}: The characteristic theorems associated with the specified
 (co)datatypes are derived rather than introduced axiomatically.%
 \footnote{However, some of the
-internal constructions and most of the internal proof obligations are skipped
+internal constructions and most of the internal proof obligations are omitted
 if the @{text quick_and_dirty} option is enabled.}
 The package is described in a number of papers
 \cite{traytel-et-al-2012,blanchette-et-al-wit,blanchette-et-al-2014-impl,panny-et-al-2014}.
@@ -1060,7 +1060,9 @@
 \item \emph{Accordingly, the induction rule is different for nested recursive
 datatypes.} Again, the old-style induction rule can be generated on demand using
 @{command primrec} if the recursion is via new-style datatypes, as explained in
-Section~\ref{sssec:primrec-nested-as-mutual-recursion}.
+Section~\ref{sssec:primrec-nested-as-mutual-recursion}. For recursion through
+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 internal constructions are completely different.} Proof texts
 that unfold the definition of constants introduced by \keyw{datatype} will be