src/Doc/Datatypes/Datatypes.thy

 %    old \keyw{datatype}
 %
 %  * @{command wrap_free_constructors}
 %    * @{text "no_discs_sels"}, @{text "rep_compat"}
 %    * hack to have both co and nonco view via locale (cf. ext nats)
+%  * code generator
+%     * eq, refl, simps
 *}
 
 
 (*
 subsection {* Introductory Example

   ;
   X_list: '[' (X + ',') ']'
 "}
 
 % options: no_discs_sels rep_compat
-
-% X_list is as for BNF
 
 \noindent
 Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
 *}