equal
deleted
inserted
replaced
122 % |
122 % |
123 \isatagmlref |
123 \isatagmlref |
124 % |
124 % |
125 \begin{isamarkuptext}% |
125 \begin{isamarkuptext}% |
126 \begin{mldecls} |
126 \begin{mldecls} |
127 \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\ |
127 \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code.read_const: theory -> string -> string| \\ |
128 \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: simpset -> thm -> thm| \\ |
128 \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\ |
129 \end{mldecls} |
129 \end{mldecls} |
130 |
130 |
131 \begin{description} |
131 \begin{description} |
132 |
132 |
133 \item \verb|Code_Unit.read_const|~\isa{thy}~\isa{s} |
133 \item \verb|Code.read_const|~\isa{thy}~\isa{s} |
134 reads a constant as a concrete term expression \isa{s}. |
134 reads a constant as a concrete term expression \isa{s}. |
135 |
135 |
136 \item \verb|Code_Unit.rewrite_eqn|~\isa{ss}~\isa{thm} |
136 \item \verb|Code.rewrite_eqn|~\isa{ss}~\isa{thm} |
137 rewrites a code equation \isa{thm} with a simpset \isa{ss}; |
137 rewrites a code equation \isa{thm} with a simpset \isa{ss}; |
138 only arguments and right hand side are rewritten, |
138 only arguments and right hand side are rewritten, |
139 not the head of the code equation. |
139 not the head of the code equation. |
140 |
140 |
141 \end{description}% |
141 \end{description}% |