src/Doc/Datatypes/Datatypes.thy

 used to ensure that the tail of the empty list is the empty list (instead of
 being left unspecified).
 
 Because @{const Nil} is a nullary constructor, it is also possible to use
 @{term "\<lambda>xs. xs = Nil"} as a discriminator. This is specified by
-entering ``@{text "="}'' instead of the identifier @{const null} in the
-declaration above. Although this may look appealing, the mixture of constructors
-and selectors in the resulting characteristic theorems can lead Isabelle's
-automation to switch between the constructor and the destructor view in
-surprising ways.
-*}
-
-text {*
+entering ``@{text "="}'' instead of the identifier @{const null}. Although this
+may look appealing, the mixture of constructors and selectors in the resulting
+characteristic theorems can lead Isabelle's automation to switch between the
+constructor and the destructor view in surprising ways.
+
 The usual mixfix syntaxes are available for both types and constructors. For
 example:
 *}
 
 (*<*)

 
 text {*
 Datatype definitions have the following general syntax:
 
 @{rail "
-  @@{command datatype_new} @{syntax target}? @{syntax dt_options}? \\
+  @@{command_def datatype_new} target? @{syntax dt_options}? \\
     (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
   ;
   @{syntax_def dt_options}: '(' ((@'no_discs_sels' | @'rep_compat') + ',') ')'
 "}
 
-The syntactic quantity @{syntax 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 followed by optional options:
+The syntactic quantity \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 optionally followed by datatype-specific options:
 
 \begin{itemize}
 \setlength{\itemsep}{0pt}
 
 \item
 The \keyw{no\_discs\_sels} option indicates that no destructors (i.e.,
 discriminators and selectors) should be generated.
 
 \item
 The \keyw{rep\_compat} option indicates that the names generated by the
-package should contain optional (and normally not displayed) @{text "new."}
+package should contain optional (and normally not displayed) ``@{text "new."}''
 components to prevent clashes with a later call to @{command rep_datatype}. See
 Section~\ref{ssec:datatype-compatibility-issues} for details.
 \end{itemize}
 
 The left-hand sides of the datatype equations specify the name of the type to
-define, its type parameters, and optional additional information:
+define, its type parameters, and additional information:
 
 @{rail "
-  @{syntax_def dt_name}: @{syntax tyargs}? @{syntax name}
-    @{syntax map_rel}? @{syntax mixfix}?
+  @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix?
   ;
-  @{syntax_def tyargs}: @{syntax typefree} | '(' ((@{syntax name} ':')? @{syntax typefree} + ',') ')'
+  @{syntax_def tyargs}: typefree | '(' ((name ':')? typefree + ',') ')'
   ;
-  @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' @{syntax name}) +) ')'
+  @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
 "}
 
 \noindent
-The syntactic quantity @{syntax name} denotes an identifier, @{syntax typefree}
-denotes fixed type variable (@{typ 'a}, @{typ 'b}, \ldots), and @{syntax
-mixfix} denotes the usual parenthesized mixfix notation. They are documented in
-the Isar reference manual \cite{isabelle-isar-ref}.
+The syntactic quantity \synt{name} denotes an identifier, \synt{typefree}
+denotes fixed type variable (@{typ 'a}, @{typ 'b}, \ldots), and \synt{mixfix}
+denotes the usual parenthesized mixfix notation. They are documented in the Isar
+reference manual \cite{isabelle-isar-ref}.
 
 The optional names preceding the type variables allow to override the default
 names of the set functions (@{text t_set1}, \ldots, @{text t_setM}).
 Inside a mutually recursive datatype specification, all defined datatypes must
 specify exactly the same type variables in the same order.
 
 @{rail "
-  @{syntax_def ctor}: (@{syntax name} ':')? @{syntax name} (@{syntax ctor_arg} * ) \\
-    @{syntax dt_sel_defaults}? @{syntax mixfix}?
+  @{syntax_def ctor}: (name ':')? name (@{syntax ctor_arg} * ) \\
+    @{syntax dt_sel_defaults}? mixfix?
 "}
 
 \noindent
 The main constituents of a constructor specification is 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 name
 (@{text t.un_C}$_{ij}$).
 
 @{rail "
-  @{syntax_def ctor_arg}: @{syntax type} | '(' @{syntax name} ':' @{syntax type} ')'
+  @{syntax_def ctor_arg}: type | '(' name ':' type ')'
 "}
 
 \noindent
 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 t.un_C}$_{ij}$). The same selector names can be reused for several
 constructors as long as they have the same type.
 
 @{rail "
-  @{syntax_def dt_sel_defaults}: '(' @'defaults' (@{syntax name} ':' @{syntax term} +) ')'
+  @{syntax_def dt_sel_defaults}: '(' @'defaults' (name ':' term +) ')'
 "}
 
 \noindent
 Given a constructor
 @{text "C \<Colon> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<sigma>"},

 
 text {*
 Primitive recursive functions have the following general syntax:
 
 @{rail "
-  @@{command primrec_new} @{syntax target}? @{syntax \"fixes\"} \\ @'where'
+  @@{command primrec_new} target? fixes \\ @'where'
     (@{syntax primrec_equation} + '|')
   ;
-  @{syntax_def primrec_equation}: @{syntax thmdecl}? @{syntax prop}
+  @{syntax_def primrec_equation}: thmdecl? prop
 "}
 *}
 
 
 subsection {* Generated Theorems

 
 text {*
 Primitive corecursive definitions have the following general syntax:
 
 @{rail "
-  @@{command primcorec} @{syntax target}? @{syntax \"fixes\"} \\ @'where'
+  @@{command primcorec} target? fixes \\ @'where'
     (@{syntax primcorec_formula} + '|')
   ;
-  @{syntax_def primcorec_formula}: @{syntax thmdecl}? @{syntax prop}
-    (@'of' (@{syntax term} * ))?
+  @{syntax_def primcorec_formula}: thmdecl? prop (@'of' (term * ))?
 "}
 *}
 
 
 subsection {* Generated Theorems

   \label{ssec:bnf-syntax} *}
 
 text {*
 
 @{rail "
-  @@{command bnf} @{syntax target}? (@{syntax name} ':')? @{syntax term} \\
-    @{syntax term_list} @{syntax term} @{syntax term_list} @{syntax term}?
+  @@{command bnf} target? (name ':')? term \\
+    term_list term term_list term?
   ;
-  @{syntax_def X_list}: '[' (@{syntax X} + ',') ']'
+  X_list: '[' (X + ',') ']'
 "}
 
 options: no_discs_sels rep_compat
 *}
 

 
 text {*
 Free constructor wrapping has the following general syntax:
 
 @{rail "
-  @@{command wrap_free_constructors} @{syntax target}? @{syntax dt_options} \\
-    @{syntax term_list} @{syntax name} @{syntax fc_discs_sels}?
+  @@{command wrap_free_constructors} target? @{syntax dt_options} \\
+    term_list name @{syntax fc_discs_sels}?
   ;
-  @{syntax_def fc_discs_sels}: @{syntax name_list} (@{syntax name_list_list} @{syntax name_term_list_list}? )?
+  @{syntax_def fc_discs_sels}: name_list (name_list_list name_term_list_list? )?
   ;
-  @{syntax_def name_term}: (@{syntax name} ':' @{syntax term})
+  @{syntax_def name_term}: (name ':' term)
 "}
 
 options: no_discs_sels rep_compat
 
 X_list is as for BNF