--- a/src/Doc/Datatypes/Datatypes.thy Fri Mar 14 09:56:06 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Mar 14 10:08:33 2014 +0100
@@ -1355,7 +1355,7 @@
\label{ssec:primrec-command-syntax} *}
-subsubsection {* \keyw{primrec\_new}
+subsubsection {* \keyw{primrec}
\label{sssec:primrec-new} *}
text {*
@@ -1364,7 +1364,10 @@
\end{matharray}
@{rail \<open>
- @@{command primrec} target? fixes \<newline> @'where' (@{syntax pr_equation} + '|')
+ @@{command primrec} target? @{syntax pr_option}? fixes \<newline>
+ @'where' (@{syntax pr_equation} + '|')
+ ;
+ @{syntax_def pr_option}: '(' 'nonexhaustive' ')'
;
@{syntax_def pr_equation}: thmdecl? prop
\<close>}
@@ -1380,6 +1383,17 @@
\synt{thmdecl} denotes an optional name for the formula that follows, and
\synt{prop} denotes a HOL proposition \cite{isabelle-isar-ref}.
+The optional target is potentially followed by a recursion-specific option:
+
+\begin{itemize}
+\setlength{\itemsep}{0pt}
+
+\item
+The @{text "nonexhaustive"} option indicates that the functions are not
+necessarily specified for all constructors. It can be used to suppress the
+warning that is normally emitted when some constructors are missing.
+\end{itemize}
+
%%% TODO: elaborate on format of the equations
%%% TODO: elaborate on mutual and nested-to-mutual
*}