# HG changeset patch
# User blanchet
# Date 1386012714 -3600
# Node ID a21a2223c02b0e7e581b56f77e820d08f401c998
# Parent  62fb5af93fe24697036ad74a730caeb8fb483c4d
minor doc update

diff -r 62fb5af93fe2 -r a21a2223c02b src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Dec 02 20:31:54 2013 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Dec 02 20:31:54 2013 +0100
@@ -2350,6 +2350,8 @@
 %  * @{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
 *}
 
 
@@ -2384,8 +2386,6 @@
 
 % options: no_discs_sels rep_compat
 
-% X_list is as for BNF
-
 \noindent
 Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
 *}