equal
deleted
inserted
replaced
76 |
76 |
77 subsection {* Auxiliary *} |
77 subsection {* Auxiliary *} |
78 |
78 |
79 text %mlref {* |
79 text %mlref {* |
80 \begin{mldecls} |
80 \begin{mldecls} |
81 @{index_ML Code.read_const: "theory -> string -> string"} \\ |
81 @{index_ML Code.read_const: "theory -> string -> string"} |
82 @{index_ML Code.rewrite_eqn: "simpset -> thm -> thm"} \\ |
|
83 \end{mldecls} |
82 \end{mldecls} |
84 |
83 |
85 \begin{description} |
84 \begin{description} |
86 |
85 |
87 \item @{ML Code.read_const}~@{text thy}~@{text s} |
86 \item @{ML Code.read_const}~@{text thy}~@{text s} |
88 reads a constant as a concrete term expression @{text s}. |
87 reads a constant as a concrete term expression @{text s}. |
89 |
|
90 \item @{ML Code.rewrite_eqn}~@{text ss}~@{text thm} |
|
91 rewrites a code equation @{text thm} with a simpset @{text ss}; |
|
92 only arguments and right hand side are rewritten, |
|
93 not the head of the code equation. |
|
94 |
88 |
95 \end{description} |
89 \end{description} |
96 |
90 |
97 *} |
91 *} |
98 |
92 |