--- a/src/Doc/Datatypes/Datatypes.thy Thu Feb 13 17:11:11 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Thu Feb 13 17:11:25 2014 +0100
@@ -476,10 +476,13 @@
\medskip
\noindent
+The @{command datatype_new} command introduces a set of mutually recursive
+datatypes specified by their constructors.
+
The syntactic entity \synt{target} can be used to specify a local
context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference
manual \cite{isabelle-isar-ref}.
-%
+
The optional target is potentially followed by datatype-specific options:
\begin{itemize}
@@ -1367,6 +1370,21 @@
;
@{syntax_def pr_equation}: thmdecl? prop
\<close>}
+
+\medskip
+
+\noindent
+The @{command primrec_new} command introduces a set of mutually recursive
+functions over a datatype.
+
+The syntactic entity \synt{target} can be used to specify a local context,
+\synt{fixes} is a list of names with optional type signatures, \synt{thmdecl}
+is an optional name for the formula that follows, and \synt{prop} is a HOL
+proposition. They are is documented in the Isar reference manual
+\cite{isabelle-isar-ref}.
+
+%%% TODO: elaborate on format of the equations
+%%% TODO: elaborate on mutual and nested-to-mutual
*}
@@ -2251,8 +2269,7 @@
@{rail \<open>
(@@{command primcorec} | @@{command primcorecursive}) target? \<newline>
- @{syntax pcr_option}? fixes @'where'
- (@{syntax pcr_formula} + '|')
+ @{syntax pcr_option}? fixes @'where' (@{syntax pcr_formula} + '|')
;
@{syntax_def pcr_option}: '(' ('sequential' | 'exhaustive') ')'
;
@@ -2262,6 +2279,15 @@
\medskip
\noindent
+The @{command primcorec} command introduces a set of mutually corecursive
+functions over a codatatype.
+
+The syntactic entity \synt{target} can be used to specify a local context,
+\synt{fixes} is a list of names with optional type signatures, \synt{thmdecl}
+is an optional name for the formula that follows, and \synt{prop} is a HOL
+proposition. They are is documented in the Isar reference manual
+\cite{isabelle-isar-ref}.
+
The optional target is potentially followed by a corecursion-specific option:
\begin{itemize}
@@ -2280,6 +2306,9 @@
\noindent
The @{command primcorec} command is an abbreviation for @{command primcorecursive} with
@{text "by auto?"} to discharge any emerging proof obligations.
+
+%%% TODO: elaborate on format of the propositions
+%%% TODO: elaborate on mutual and nested-to-mutual
*}
@@ -2479,6 +2508,18 @@
'map:' term ('sets:' (term +))? 'bd:' term \<newline>
('wits:' (term +))? ('rel:' term)?
\<close>}
+
+\medskip
+
+\noindent
+The @{command bnf} command registers an existing type as a bounded natural
+functor (BNF). The type must be equipped with an appropriate map function
+(functorial action). In addition, custom set functions, relators, and
+nonemptiness witnesses can be specified; otherwise, default versions are used.
+
+The syntactic entity \synt{target} can be used to specify a local
+context---e.g., @{text "(in linorder)"}. It is documented in the Isar
+reference manual \cite{isabelle-isar-ref}.
*}
@@ -2508,12 +2549,17 @@
\noindent
The @{command bnf_decl} command declares a new type and associated constants
(map, set, relator, and cardinal bound) and asserts the BNF properties for
-these constants as axioms. Type arguments are live by default; they can be
-marked as dead by entering ``-'' (hyphen) instead of an identifier for the
-corresponding set function. Witnesses can be specified by their types.
-Otherwise, the syntax of @{command bnf_decl} is
-identical to the left-hand side of a @{command datatype_new} or @{command
-codatatype} definition.
+these constants as axioms.
+
+The syntactic entity \synt{target} can be used to specify a local
+context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference
+manual \cite{isabelle-isar-ref}.
+
+Type arguments are live by default; they can be marked as dead by entering
+``-'' (hyphen) instead of an identifier for the corresponding set function.
+Witnesses can be specified by their types. Otherwise, the syntax of
+@{command bnf_decl} is identical to the left-hand side of a
+@{command datatype_new} or @{command codatatype} definition.
The command is useful to reason abstractly about BNFs. The axioms are safe
because there exists BNFs of arbitrary large arities. Applications must import
@@ -2589,9 +2635,18 @@
\medskip
+\noindent
+The @{command free_constructors} command generates destructor constants for
+freely constructed types as well as properties about constructors and
+destructors. It also registers the constants and theorems in a data structure
+that is queried by various tools (e.g., \keyw{function}).
+
+The syntactic entity \synt{target} can be used to specify a local
+context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference
+manual \cite{isabelle-isar-ref}.
+
% options: no_discs_sels no_code
-\noindent
Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
For technical reasons, the @{text "[fundef_cong]"} attribute is not set on the
generated @{text case_cong} theorem. It can be added manually using