1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Nov 27 15:08:18 2013 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Wed Nov 27 15:34:07 2013 +0100
     1.3 @@ -2290,7 +2290,6 @@
     1.4  *}
     1.5  
     1.6  
     1.7 -(* NOTYET
     1.8  subsubsection {* \keyw{bnf\_decl}
     1.9    \label{sssec:bnf-decl} *}
    1.10  
    1.11 @@ -2301,10 +2300,23 @@
    1.12  \end{matharray}
    1.13  
    1.14  @{rail "
    1.15 -  @@{command bnf} target? dt_name
    1.16 +  @@{command bnf_decl} target? @{syntax dt_name}
    1.17 +  ;
    1.18 +  @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix?
    1.19 +  ;
    1.20 +  @{syntax_def tyargs}: typefree | '(' (((name | '-') ':')? typefree + ',') ')'
    1.21 +  ;
    1.22 +  @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
    1.23  "}
    1.24 +
    1.25 +Declares a fresh type and fresh constants (map, set, relator, cardinal bound)
    1.26 +and asserts the bnf properties for these constants as axioms. Additionally,
    1.27 +type arguments may be marked as dead (by using @{syntax "-"} instead of a name for the
    1.28 +set function)---this is the only difference of @{syntax dt_name} compared to
    1.29 +the syntax used by the @{command datatype_new}/@{command codatatype} commands.
    1.30 +
    1.31 +The axioms are sound, since one there exists a bnf of any given arity.
    1.32  *}
    1.33 -*)
    1.34  
    1.35  
    1.36  subsubsection {* \keyw{print\_bnfs}