# HG changeset patch
# User traytel
# Date 1385562847 -3600
# Node ID 16879025203875c82d7904bd3e0a02d9e790084b
# Parent  91a1e4aa7c803ead3728ed2c6a4372f98e841596
some documentation

diff -r 91a1e4aa7c80 -r 168790252038 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Nov 27 15:08:18 2013 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Nov 27 15:34:07 2013 +0100
@@ -2290,7 +2290,6 @@
 *}
 
 
-(* NOTYET
 subsubsection {* \keyw{bnf\_decl}
   \label{sssec:bnf-decl} *}
 
@@ -2301,10 +2300,23 @@
 \end{matharray}
 
 @{rail "
-  @@{command bnf} target? dt_name
+  @@{command bnf_decl} target? @{syntax dt_name}
+  ;
+  @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix?
+  ;
+  @{syntax_def tyargs}: typefree | '(' (((name | '-') ':')? typefree + ',') ')'
+  ;
+  @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
 "}
+
+Declares a fresh type and fresh constants (map, set, relator, cardinal bound)
+and asserts the bnf properties for these constants as axioms. Additionally,
+type arguments may be marked as dead (by using @{syntax "-"} instead of a name for the
+set function)---this is the only difference of @{syntax dt_name} compared to
+the syntax used by the @{command datatype_new}/@{command codatatype} commands.
+
+The axioms are sound, since one there exists a bnf of any given arity.
 *}
-*)
 
 
 subsubsection {* \keyw{print\_bnfs}