--- 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.
*}