updated to changes in sources; tuned
authorhaftmann
Tue Jul 14 10:54:21 2009 +0200 (2009-07-14)
changeset 31999cb1f26c0de5b
parent 31998 2c7a24f74db9
child 32000 6f07563dc8a9
updated to changes in sources; tuned
doc-src/Codegen/Thy/ML.thy
     1.1 --- a/doc-src/Codegen/Thy/ML.thy	Tue Jul 14 10:54:04 2009 +0200
     1.2 +++ b/doc-src/Codegen/Thy/ML.thy	Tue Jul 14 10:54:21 2009 +0200
     1.3 @@ -78,8 +78,7 @@
     1.4  
     1.5  text %mlref {*
     1.6    \begin{mldecls}
     1.7 -  @{index_ML Code.read_const: "theory -> string -> string"} \\
     1.8 -  @{index_ML Code.rewrite_eqn: "simpset -> thm -> thm"} \\
     1.9 +  @{index_ML Code.read_const: "theory -> string -> string"}
    1.10    \end{mldecls}
    1.11  
    1.12    \begin{description}
    1.13 @@ -87,11 +86,6 @@
    1.14    \item @{ML Code.read_const}~@{text thy}~@{text s}
    1.15       reads a constant as a concrete term expression @{text s}.
    1.16  
    1.17 -  \item @{ML Code.rewrite_eqn}~@{text ss}~@{text thm}
    1.18 -     rewrites a code equation @{text thm} with a simpset @{text ss};
    1.19 -     only arguments and right hand side are rewritten,
    1.20 -     not the head of the code equation.
    1.21 -
    1.22    \end{description}
    1.23  
    1.24  *}