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