equal
deleted
inserted
replaced
199 \end{matharray} |
199 \end{matharray} |
200 |
200 |
201 @{rail " |
201 @{rail " |
202 @@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref} |
202 @@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref} |
203 ; |
203 ; |
204 @@{method split} ('(' 'asm' ')')? @{syntax thmrefs} |
204 @@{method split} @{syntax thmrefs} |
205 "} |
205 "} |
206 |
206 |
207 These methods provide low-level facilities for equational reasoning |
207 These methods provide low-level facilities for equational reasoning |
208 that are intended for specialized applications only. Normally, |
208 that are intended for specialized applications only. Normally, |
209 single step calculations would be performed in a structured text |
209 single step calculations would be performed in a structured text |
243 \item @{method hypsubst} performs substitution using some |
243 \item @{method hypsubst} performs substitution using some |
244 assumption; this only works for equations of the form @{text "x = |
244 assumption; this only works for equations of the form @{text "x = |
245 t"} where @{text x} is a free or bound variable. |
245 t"} where @{text x} is a free or bound variable. |
246 |
246 |
247 \item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case |
247 \item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case |
248 splitting using the given rules. By default, splitting is performed |
248 splitting using the given rules. Splitting is performed in the |
249 in the conclusion of a goal; the @{text "(asm)"} option indicates to |
249 conclusion or some assumption of the subgoal, depending of the |
250 operate on assumptions instead. |
250 structure of the rule. |
251 |
251 |
252 Note that the @{method simp} method already involves repeated |
252 Note that the @{method simp} method already involves repeated |
253 application of split rules as declared in the current context. |
253 application of split rules as declared in the current context, using |
|
254 @{attribute split}, for example. |
254 |
255 |
255 \end{description} |
256 \end{description} |
256 *} |
257 *} |
257 |
258 |
258 |
259 |