--- a/src/Doc/Datatypes/Datatypes.thy Mon Mar 16 17:01:59 2015 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Mar 16 17:02:00 2015 +0100
@@ -552,7 +552,8 @@
\noindent
The main constituents of a constructor specification are the name of the
constructor and the list of its argument types. An optional discriminator name
-can be supplied at the front to override the default, which is
+can be supplied at the front. If discriminators are enabled (cf.\ the
+@{text "discs_sels"} option) but no name is supplied, the default is
@{text "\<lambda>x. x = C\<^sub>j"} for nullary constructors and
@{text t.is_C\<^sub>j} otherwise.
@@ -566,9 +567,10 @@
The syntactic entity \synt{type} denotes a HOL type @{cite "isabelle-isar-ref"}.
In addition to the type of a constructor argument, it is possible to specify a
-name for the corresponding selector to override the default name
-(@{text un_C\<^sub>ji}). The same selector names can be reused for several
-constructors as long as they share the same type.
+name for the corresponding selector. The same selector name can be reused for
+arguments to several constructors as long as the arguments share the same type.
+If selectors are enabled (cf.\ the @{text "discs_sels"} option) but no name is
+supplied, the default name is @{text un_C\<^sub>ji}.
*}
@@ -614,9 +616,7 @@
@{text compat_tree.rec}).
\item All types through which recursion takes place must be new-style datatypes
-or the function type. In principle, it should be possible to support old-style
-datatypes as well, but this has not been implemented yet (and there is currently
-no way to register old-style datatypes as new-style datatypes).
+or the function type.
\end{itemize}
*}
@@ -625,7 +625,7 @@
\label{ssec:datatype-generated-constants} *}
text {*
-Given a datatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"} with $m > 0$ live type variables
+Given a datatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"} with $m$ live type variables
and $n$ constructors @{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the following
auxiliary constants are introduced:
@@ -653,6 +653,10 @@
\medskip
\noindent
+The discriminators and selectors are generated only if the @{text "discs_sels"}
+option is enabled or if names are specified for discriminators or selectors.
+The set functions, map function, and relator are generated only if $m > 0$.
+
In addition, some of the plugins introduce their own constants
(Section~\ref{sec:selecting-plugins}). The case combinator, discriminators,
and selectors are collectively called \emph{destructors}. The prefix
@@ -3226,8 +3230,8 @@
Kun\v{c}ar implemented the @{text transfer} and @{text lifting} plugins.
Florian Haftmann and Christian Urban provided general advice on Isabelle and
package writing. Stefan Milius and Lutz Schr\"oder found an elegant proof that
-eliminated one of the BNF proof obligations. Andreas Lochbihler and Christian
-Sternagel suggested many textual improvements to this tutorial.
+eliminated one of the BNF proof obligations. Andreas Lochbihler, Tobias Nipkow,
+and Christian Sternagel suggested many textual improvements to this tutorial.
*}
end