updated
authorhaftmann
Fri, 24 Oct 2008 10:41:15 +0200
changeset 28680f1c76cf10915
parent 28679 d7384e8e99b3
child 28681 e8664643f543
updated
doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex	Fri Oct 24 10:41:13 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex	Fri Oct 24 10:41:15 2008 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4  \begin{mldecls}
     1.5    \indexml{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
     1.6    \indexml{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
     1.7 -  \indexml{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list Susp.T -> theory -> theory| \\
     1.8 +  \indexml{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list Lazy.T -> theory -> theory| \\
     1.9    \indexml{Code.map\_pre}\verb|Code.map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\
    1.10    \indexml{Code.map\_post}\verb|Code.map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\
    1.11    \indexml{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%