doc-src/Codegen/Thy/document/Further.tex
changeset 38734 9cea8a0e925a
parent 38730 2f8699695cf6
child 38735 ec0408c7328b
     1.1 --- a/doc-src/Codegen/Thy/document/Further.tex	Wed Aug 18 10:07:56 2010 +0200
     1.2 +++ b/doc-src/Codegen/Thy/document/Further.tex	Wed Aug 18 10:07:57 2010 +0200
     1.3 @@ -415,8 +415,9 @@
     1.4    \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
     1.5    \indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\
     1.6    \indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\
     1.7 -  \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
     1.8 -\verb|    -> theory -> theory| \\
     1.9 +  \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: |\isasep\isanewline%
    1.10 +\verb|    string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
    1.11 +\verb|      -> theory -> theory| \\
    1.12    \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
    1.13    \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
    1.14    \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%