# HG changeset patch
# User wenzelm
# Date 1210278755 -7200
# Node ID 610ca045b1b25a10539c6c5573402915a573c09d
# Parent  7bb3d2ee0606d59bef47b0e18fdac43d6d5454f8
updated generated file;

diff -r 7bb3d2ee0606 -r 610ca045b1b2 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu May 08 22:31:23 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu May 08 22:32:35 2008 +0200
@@ -1478,21 +1478,21 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{Code.add-func}\verb|Code.add_func: thm -> theory -> theory| \\
-  \indexml{Code.del-func}\verb|Code.del_func: thm -> theory -> theory| \\
-  \indexml{Code.add-funcl}\verb|Code.add_funcl: string * thm list Susp.T -> theory -> theory| \\
-  \indexml{Code.add-inline}\verb|Code.add_inline: thm -> theory -> theory| \\
-  \indexml{Code.del-inline}\verb|Code.del_inline: thm -> theory -> theory| \\
-  \indexml{Code.add-inline-proc}\verb|Code.add_inline_proc: string * (theory -> cterm list -> thm list)|\isasep\isanewline%
+  \indexml{Code.add\_func}\verb|Code.add_func: thm -> theory -> theory| \\
+  \indexml{Code.del\_func}\verb|Code.del_func: thm -> theory -> theory| \\
+  \indexml{Code.add\_funcl}\verb|Code.add_funcl: string * thm list Susp.T -> theory -> theory| \\
+  \indexml{Code.add\_inline}\verb|Code.add_inline: thm -> theory -> theory| \\
+  \indexml{Code.del\_inline}\verb|Code.del_inline: thm -> theory -> theory| \\
+  \indexml{Code.add\_inline\_proc}\verb|Code.add_inline_proc: string * (theory -> cterm list -> thm list)|\isasep\isanewline%
 \verb|    -> theory -> theory| \\
-  \indexml{Code.del-inline-proc}\verb|Code.del_inline_proc: string -> theory -> theory| \\
-  \indexml{Code.add-preproc}\verb|Code.add_preproc: string * (theory -> thm list -> thm list)|\isasep\isanewline%
+  \indexml{Code.del\_inline\_proc}\verb|Code.del_inline_proc: string -> theory -> theory| \\
+  \indexml{Code.add\_preproc}\verb|Code.add_preproc: string * (theory -> thm list -> thm list)|\isasep\isanewline%
 \verb|    -> theory -> theory| \\
-  \indexml{Code.del-preproc}\verb|Code.del_preproc: string -> theory -> theory| \\
-  \indexml{Code.add-datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
-  \indexml{Code.get-datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
+  \indexml{Code.del\_preproc}\verb|Code.del_preproc: string -> theory -> theory| \\
+  \indexml{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
+  \indexml{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
 \verb|    -> (string * sort) list * (string * typ list) list| \\
-  \indexml{Code.get-datatype-of-constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option|
+  \indexml{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option|
   \end{mldecls}
 
   \begin{description}
@@ -1564,9 +1564,9 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{CodeUnit.read-const}\verb|CodeUnit.read_const: theory -> string -> string| \\
-  \indexml{CodeUnit.head-func}\verb|CodeUnit.head_func: thm -> string * typ| \\
-  \indexml{CodeUnit.rewrite-func}\verb|CodeUnit.rewrite_func: thm list -> thm -> thm| \\
+  \indexml{CodeUnit.read\_const}\verb|CodeUnit.read_const: theory -> string -> string| \\
+  \indexml{CodeUnit.head\_func}\verb|CodeUnit.head_func: thm -> string * typ| \\
+  \indexml{CodeUnit.rewrite\_func}\verb|CodeUnit.rewrite_func: thm list -> thm -> thm| \\
   \end{mldecls}
 
   \begin{description}