# HG changeset patch
# User blanchet
# Date 1378905763 -7200
# Node ID de2027f9aff3da94c5a2264d877d4f19ff1cd6c6
# Parent  24ce26e8af1296d3fc0bd585c95dbdcce5621975
more (co)datatype documentation

diff -r 24ce26e8af12 -r de2027f9aff3 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Sep 11 14:07:24 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Sep 11 15:22:43 2013 +0200
@@ -400,14 +400,11 @@
 
 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.
-*}
+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.
 
-text {*
 The usual mixfix syntaxes are available for both types and constructors. For
 example:
 *}
@@ -440,17 +437,17 @@
 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}
@@ -461,28 +458,27 @@
 
 \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}).
@@ -490,8 +486,8 @@
 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
@@ -501,7 +497,7 @@
 (@{text t.un_C}$_{ij}$).
 
 @{rail "
-  @{syntax_def ctor_arg}: @{syntax type} | '(' @{syntax name} ':' @{syntax type} ')'
+  @{syntax_def ctor_arg}: type | '(' name ':' type ')'
 "}
 
 \noindent
@@ -511,7 +507,7 @@
 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
@@ -811,10 +807,10 @@
 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
 "}
 *}
 
@@ -966,11 +962,10 @@
 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 * ))?
 "}
 *}
 
@@ -1011,10 +1006,10 @@
 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
@@ -1050,12 +1045,12 @@
 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
diff -r 24ce26e8af12 -r de2027f9aff3 src/Doc/Datatypes/document/root.tex
--- a/src/Doc/Datatypes/document/root.tex	Wed Sep 11 14:07:24 2013 +0200
+++ b/src/Doc/Datatypes/document/root.tex	Wed Sep 11 15:22:43 2013 +0200
@@ -18,6 +18,7 @@
 \parindent=4\wd\boxA
 
 \newcommand{\keyw}[1]{\isacommand{#1}}
+\newcommand{\synt}[1]{\textit{#1}}
 
 %\renewcommand{\isactrlsub}[1]{\/$\sb{\mathrm{#1}}$}
 \renewcommand{\isactrlsub}[1]{\/$\sb{#1}$}