# 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